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 -> ( ph <-> ps ) )
	ichcircshi.2	|- ( y = x -> ( ps <-> ch ) )
	ichcircshi.3	|- ( z = y -> ( ch <-> ph ) )
Assertion	ichcircshi	|- [ x <> y ] ph

Proof

Step	Hyp	Ref	Expression
1		ichcircshi.1	|- ( x = z -> ( ph <-> ps ) )
2		ichcircshi.2	|- ( y = x -> ( ps <-> ch ) )
3		ichcircshi.3	|- ( z = y -> ( ch <-> ph ) )
4	3	bicomd	|- ( z = y -> ( ph <-> ch ) )
5	4	equcoms	|- ( y = z -> ( ph <-> ch ) )
6	5	sbievw	|- ( [ z / y ] ph <-> ch )
7	6	2sbbii	|- ( [ x / z ] [ y / x ] [ z / y ] ph <-> [ x / z ] [ y / x ] ch )
8	2	bicomd	|- ( y = x -> ( ch <-> ps ) )
9	8	equcoms	|- ( x = y -> ( ch <-> ps ) )
10	9	sbievw	|- ( [ y / x ] ch <-> ps )
11	10	sbbii	|- ( [ x / z ] [ y / x ] ch <-> [ x / z ] ps )
12	1	bicomd	|- ( x = z -> ( ps <-> ph ) )
13	12	equcoms	|- ( z = x -> ( ps <-> ph ) )
14	13	sbievw	|- ( [ x / z ] ps <-> ph )
15	7 11 14	3bitri	|- ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph )
16	15	gen2	|- A. x A. y ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph )
17		df-ich	|- ( [ x <> y ] ph <-> A. x A. y ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph ) )
18	16 17	mpbir	|- [ x <> y ] ph