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