Deux programmes sont en équivalence mutuelle s'ils divergent tous les deux ou s'ils terminent dans des états similaires. L'équivalence mutuelle est une notion adéquate d'équivalence pour les programmes déterministes. Elle est utile dans divers contextes, parmi lesquels on peut citer la preuve de transformations de programmes dans un langage donné, et la preuve de compilateurs entre deux langages. Dans cet article nous introduisons un système déductif pour l'équivalence mutuelle, qui a comme paramètres les sémantiques opérationnelles de deux langages ainsi qu'une relation de similitude entre états des programmes. Le système déductif est correct: lorsqu'il termine, il démontre l'équivalence des programmes qui lui sont donnés en entrée. Nous l'illustrons sur deux programmes, appartenant à des langages différents : l'un impératif, l'autre fonctionnel, qui calculent la séquence de Collatz de deux manières différentes.