Metamath Proof Explorer

Theorem sbco4lemOLD

Description: Obsolete version of sbco4lem as of 12-Oct-2024. (Contributed by Jim Kingdon, 26-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbco4lemOLD 
|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )

Proof

Step Hyp Ref Expression
1 sbcom2 
 |-  ( [ w / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ y / x ] [ w / v ] [ v / w ] [ w / y ] ph )
2 1 sbbii 
 |-  ( [ x / w ] [ w / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / w ] [ y / x ] [ w / v ] [ v / w ] [ w / y ] ph )
3 sbco2vv 
 |-  ( [ v / w ] [ w / y ] ph <-> [ v / y ] ph )
4 3 sbbii 
 |-  ( [ y / x ] [ v / w ] [ w / y ] ph <-> [ y / x ] [ v / y ] ph )
5 4 2sbbii 
 |-  ( [ x / w ] [ w / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / w ] [ w / v ] [ y / x ] [ v / y ] ph )
6 sbco2vv 
 |-  ( [ x / w ] [ w / v ] [ y / x ] [ v / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph )
7 5 6 bitri 
 |-  ( [ x / w ] [ w / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph )
8 sbid2vw 
 |-  ( [ w / v ] [ v / w ] [ w / y ] ph <-> [ w / y ] ph )
9 8 2sbbii 
 |-  ( [ x / w ] [ y / x ] [ w / v ] [ v / w ] [ w / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
10 2 7 9 3bitr3i 
 |-  ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )