Metamath Proof Explorer


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 [ 𝑥𝑦 ] 𝜑