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 ⊢ x = z → φ ↔ ψ
ichcircshi.2 ⊢ y = x → ψ ↔ χ
ichcircshi.3 ⊢ z = y → χ ↔ φ
Assertion ichcircshi ⊢ x ⇄ y φ

Proof

Step Hyp Ref Expression
1 ichcircshi.1 ⊢ x = z → φ ↔ ψ
2 ichcircshi.2 ⊢ y = x → ψ ↔ χ
3 ichcircshi.3 ⊢ z = y → χ ↔ φ
4 3 bicomd ⊢ z = y → φ ↔ χ
5 4 equcoms ⊢ y = z → φ ↔ χ
6 5 sbievw ⊢ z y φ ↔ χ
7 6 2sbbii ⊢ x z y x z y φ ↔ x z y x χ
8 2 bicomd ⊢ y = x → χ ↔ ψ
9 8 equcoms ⊢ x = y → χ ↔ ψ
10 9 sbievw ⊢ y x χ ↔ ψ
11 10 sbbii ⊢ x z y x χ ↔ x z ψ
12 1 bicomd ⊢ x = z → ψ ↔ φ
13 12 equcoms ⊢ z = x → ψ ↔ φ
14 13 sbievw ⊢ x z ψ ↔ φ
15 7 11 14 3bitri ⊢ x z y x z y φ ↔ φ
16 15 gen2 ⊢ ∀ x ∀ y x z y x z y φ ↔ φ
17 df-ich ⊢ x ⇄ y φ ↔ ∀ x ∀ y x z y x z y φ ↔ φ
18 16 17 mpbir ⊢ x ⇄ y φ