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\to \left(\phi \leftrightarrow \psi \right)$$
	ichcircshi.2	$$⊢y=x\to \left(\psi \leftrightarrow \chi \right)$$
	ichcircshi.3	$$⊢z=y\to \left(\chi \leftrightarrow \phi \right)$$
Assertion	ichcircshi	$$⊢\left[x\rightleftarrows y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		ichcircshi.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
2		ichcircshi.2	$$⊢y=x\to \left(\psi \leftrightarrow \chi \right)$$
3		ichcircshi.3	$$⊢z=y\to \left(\chi \leftrightarrow \phi \right)$$
4	3	bicomd	$$⊢z=y\to \left(\phi \leftrightarrow \chi \right)$$
5	4	equcoms	$$⊢y=z\to \left(\phi \leftrightarrow \chi \right)$$
6	5	sbievw	$$⊢\left[z/y\right]\phi \leftrightarrow \chi$$
7	6	2sbbii	$$⊢\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \left[x/z\right]\left[y/x\right]\chi$$
8	2	bicomd	$$⊢y=x\to \left(\chi \leftrightarrow \psi \right)$$
9	8	equcoms	$$⊢x=y\to \left(\chi \leftrightarrow \psi \right)$$
10	9	sbievw	$$⊢\left[y/x\right]\chi \leftrightarrow \psi$$
11	10	sbbii	$$⊢\left[x/z\right]\left[y/x\right]\chi \leftrightarrow \left[x/z\right]\psi$$
12	1	bicomd	$$⊢x=z\to \left(\psi \leftrightarrow \phi \right)$$
13	12	equcoms	$$⊢z=x\to \left(\psi \leftrightarrow \phi \right)$$
14	13	sbievw	$$⊢\left[x/z\right]\psi \leftrightarrow \phi$$
15	7 11 14	3bitri	$$⊢\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi$$
16	15	gen2	$$⊢\forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)$$
17		df-ich	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)$$
18	16 17	mpbir	$$⊢\left[x\rightleftarrows y\right]\phi$$