Theorem icht

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

	Ref	Expression
Hypothesis	icht.1	⊢ 𝜑
Assertion	icht	⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑

Proof

Step	Hyp	Ref	Expression
1		icht.1	⊢ 𝜑
2	1	sbt	⊢ [ 𝑎 / 𝑦 ] 𝜑
3	2	sbt	⊢ [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑
4	3	sbt	⊢ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑
5	4 1	2th	⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 )
6	5	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 )
7		df-ich	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
8	6 7	mpbir	⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑