Metamath Proof Explorer

Theorem 2pm13.193

Description: pm13.193 for two variables. pm13.193 is Theorem *13.193 in WhiteheadRussell p. 179. Derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2pm13.193 
|- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> x = u )
2 simplr 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> y = v )
3 simpr 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> [ u / x ] [ v / y ] ph )
4 sbequ2 
 |-  ( x = u -> ( [ u / x ] [ v / y ] ph -> [ v / y ] ph ) )
5 1 3 4 sylc 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> [ v / y ] ph )
6 sbequ2 
 |-  ( y = v -> ( [ v / y ] ph -> ph ) )
7 2 5 6 sylc 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ph )
8 1 2 7 jca31 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( ( x = u /\ y = v ) /\ ph ) )
9 simpll 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> x = u )
10 simplr 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> y = v )
11 simpr 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ph )
12 sbequ1 
 |-  ( y = v -> ( ph -> [ v / y ] ph ) )
13 10 11 12 sylc 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> [ v / y ] ph )
14 sbequ1 
 |-  ( x = u -> ( [ v / y ] ph -> [ u / x ] [ v / y ] ph ) )
15 9 13 14 sylc 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> [ u / x ] [ v / y ] ph )
16 9 10 15 jca31 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
17 8 16 impbii 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )