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 
|- ( 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