Metamath Proof Explorer

Theorem sbco4lemOLD

Description: Obsolete version of sbco4lem as of 3-Sep-2025. (Contributed by Jim Kingdon, 26-Sep-2018) (Proof shortened by Wolf Lammen, 12-Oct-2024) (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 
 |-  ( [ y / x ] [ v / w ] [ w / y ] ph <-> [ v / w ] [ y / x ] [ w / y ] ph )
2 1 sbbii 
 |-  ( [ x / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / v ] [ v / w ] [ y / x ] [ w / y ] ph )
3 sbco2vv 
 |-  ( [ v / w ] [ w / y ] ph <-> [ v / y ] ph )
4 3 2sbbii 
 |-  ( [ x / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph )
5 sbco2vv 
 |-  ( [ x / v ] [ v / w ] [ y / x ] [ w / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
6 2 4 5 3bitr3i 
 |-  ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )