Metamath Proof Explorer

Theorem sbco4OLD

Description: Obsolete version of sbco4 as of 3-Sep-2025. (Contributed by Jim Kingdon, 25-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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