This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ichcircshi

Description: The setvar variables are interchangeable if they can be circularily shifted using a third setvar variable, using implicit substitution. (Contributed by AV, 29-Jul-2023)

Ref Expression
Hypotheses ichcircshi.1 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
ichcircshi.2 ⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜒 ) )
ichcircshi.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜒 ↔ 𝜑 ) )
Assertion ichcircshi [ 𝑥 ⇄ 𝑦 ] 𝜑

Proof

Step Hyp Ref Expression
1 ichcircshi.1 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2 ichcircshi.2 ⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜒 ) )
3 ichcircshi.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜒 ↔ 𝜑 ) )
4 3 bicomd ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
5 4 equcoms ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
6 5 sbievw ⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜒 )
7 6 2sbbii ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜒 )
8 2 bicomd ⊢ ( 𝑦 = 𝑥 → ( 𝜒 ↔ 𝜓 ) )
9 8 equcoms ⊢ ( 𝑥 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
10 9 sbievw ⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜓 )
11 10 sbbii ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜒 ↔ [ 𝑥 / 𝑧 ] 𝜓 )
12 1 bicomd ⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜑 ) )
13 12 equcoms ⊢ ( 𝑧 = 𝑥 → ( 𝜓 ↔ 𝜑 ) )
14 13 sbievw ⊢ ( [ 𝑥 / 𝑧 ] 𝜓 ↔ 𝜑 )
15 7 11 14 3bitri ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 )
16 15 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 )
17 df-ich ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
18 16 17 mpbir ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑