Metamath Proof Explorer

Theorem 2pm13.193VD

Description: Virtual deduction proof of 2pm13.193 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 2pm13.193 is 2pm13.193VD without virtual deductions and was automatically derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
2:1: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( x = u /\ y = v ) ).
3:2: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. x = u ).
4:1: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ u / x ] [ v / y ] ph ).
5:3,4: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
6:5: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ x = u ) ).
7:6: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ v / y ] ph ).
8:2: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. y = v ).
9:7,8: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ y = v ) ).
10:9: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ph /\ y = v ) ).
11:10: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ph ).
12:2,11: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
13:12: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( ( x = u /\ y = v ) /\ ph ) )
14:: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
15:14: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( x = u /\ y = v ) ).
16:15: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. y = v ).
17:14: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ph ).
18:16,17: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ph /\ y = v ) ).
19:18: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ y = v ) ).
20:15: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. x = u ).
21:19: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ v / y ] ph ).
22:20,21: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ x = u ) ).
23:22: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
24:23: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ u / x ] [ v / y ] ph ).
25:15,24: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
26:25: |- ( ( ( x = u /\ y = v ) /\ ph ) -> ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
qed:13,26: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )

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

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
2 simpl 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( x = u /\ y = v ) )
3 1 2 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( x = u /\ y = v ) ).
4 simpl 
 |-  ( ( x = u /\ y = v ) -> x = u )
5 3 4 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. x = u ).
6 simpr 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> [ u / x ] [ v / y ] ph )
7 1 6 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ u / x ] [ v / y ] ph ).
8 pm3.21 
 |-  ( x = u -> ( [ u / x ] [ v / y ] ph -> ( [ u / x ] [ v / y ] ph /\ x = u ) ) )
9 5 7 8 e11 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
10 sbequ2 
 |-  ( x = u -> ( [ u / x ] [ v / y ] ph -> [ v / y ] ph ) )
11 10 imdistanri 
 |-  ( ( [ u / x ] [ v / y ] ph /\ x = u ) -> ( [ v / y ] ph /\ x = u ) )
12 9 11 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ x = u ) ).
13 simpl 
 |-  ( ( [ v / y ] ph /\ x = u ) -> [ v / y ] ph )
14 12 13 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ v / y ] ph ).
15 simpr 
 |-  ( ( x = u /\ y = v ) -> y = v )
16 3 15 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. y = v ).
17 pm3.2 
 |-  ( [ v / y ] ph -> ( y = v -> ( [ v / y ] ph /\ y = v ) ) )
18 14 16 17 e11 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ y = v ) ).
19 sbequ2 
 |-  ( y = v -> ( [ v / y ] ph -> ph ) )
20 19 imdistanri 
 |-  ( ( [ v / y ] ph /\ y = v ) -> ( ph /\ y = v ) )
21 18 20 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ph /\ y = v ) ).
22 simpl 
 |-  ( ( ph /\ y = v ) -> ph )
23 21 22 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ph ).
24 pm3.2 
 |-  ( ( x = u /\ y = v ) -> ( ph -> ( ( x = u /\ y = v ) /\ ph ) ) )
25 3 23 24 e11 
 |-  (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
26 25 in1 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( ( x = u /\ y = v ) /\ ph ) )
27 idn1 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
28 simpl 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ( x = u /\ y = v ) )
29 27 28 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( x = u /\ y = v ) ).
30 29 4 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. x = u ).
31 29 15 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. y = v ).
32 simpr 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ph )
33 27 32 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ph ).
34 pm3.21 
 |-  ( y = v -> ( ph -> ( ph /\ y = v ) ) )
35 31 33 34 e11 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ph /\ y = v ) ).
36 sbequ1 
 |-  ( y = v -> ( ph -> [ v / y ] ph ) )
37 36 imdistanri 
 |-  ( ( ph /\ y = v ) -> ( [ v / y ] ph /\ y = v ) )
38 35 37 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ y = v ) ).
39 simpl 
 |-  ( ( [ v / y ] ph /\ y = v ) -> [ v / y ] ph )
40 38 39 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. [ v / y ] ph ).
41 pm3.21 
 |-  ( x = u -> ( [ v / y ] ph -> ( [ v / y ] ph /\ x = u ) ) )
42 30 40 41 e11 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ x = u ) ).
43 sbequ1 
 |-  ( x = u -> ( [ v / y ] ph -> [ u / x ] [ v / y ] ph ) )
44 43 imdistanri 
 |-  ( ( [ v / y ] ph /\ x = u ) -> ( [ u / x ] [ v / y ] ph /\ x = u ) )
45 42 44 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
46 simpl 
 |-  ( ( [ u / x ] [ v / y ] ph /\ x = u ) -> [ u / x ] [ v / y ] ph )
47 45 46 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. [ u / x ] [ v / y ] ph ).
48 pm3.2 
 |-  ( ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph -> ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) )
49 29 47 48 e11 
 |-  (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
50 49 in1 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
51 26 50 impbii 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )