Metamath Proof Explorer

Theorem sbco4lem

Description: Lemma for sbco4 . It replaces the temporary variable v with another temporary variable w . (Contributed by Jim Kingdon, 26-Sep-2018)

Ref Expression
Assertion sbco4lem 
|- ( [ 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 )