Metamath Proof Explorer


Theorem icht

Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)

Ref Expression
Hypothesis icht.1
|- ph
Assertion icht
|- [ x <> y ] ph

Proof

Step Hyp Ref Expression
1 icht.1
 |-  ph
2 1 sbt
 |-  [ a / y ] ph
3 2 sbt
 |-  [ y / x ] [ a / y ] ph
4 3 sbt
 |-  [ x / a ] [ y / x ] [ a / y ] ph
5 4 1 2th
 |-  ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
6 5 gen2
 |-  A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
7 df-ich
 |-  ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) )
8 6 7 mpbir
 |-  [ x <> y ] ph