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