Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2pm13.193VD Unicode version

Theorem 2pm13.193VD 28995
Description: Virtual deduction proof of 2pm13.193 28617. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 2pm13.193 28617 is 2pm13.193VD 28995 without virtual deductions and was automatically derived from 2pm13.193VD 28995. (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 ) )
Assertion
Ref Expression
2pm13.193VD  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )

Proof of Theorem 2pm13.193VD
StepHypRef Expression
1 idn1 28641 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) ).
2 simpl 443 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( x  =  u  /\  y  =  v ) )
31, 2e1_ 28704 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( x  =  u  /\  y  =  v ) ).
4 simpl 443 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
53, 4e1_ 28704 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  x  =  u ).
6 simpr 447 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  [ u  /  x ] [ v  / 
y ] ph )
71, 6e1_ 28704 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  [ u  /  x ] [ v  /  y ] ph ).
8 pm3.21 435 . . . . . . . . . 10  |-  ( x  =  u  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  ( [
u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ) )
95, 7, 8e11 28765 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ u  /  x ] [ v  / 
y ] ph  /\  x  =  u ) ).
10 sbequ2 1640 . . . . . . . . . 10  |-  ( x  =  u  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  [ v  /  y ] ph ) )
1110imdistanri 672 . . . . . . . . 9  |-  ( ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u )  ->  ( [ v  /  y ] ph  /\  x  =  u ) )
129, 11e1_ 28704 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ v  / 
y ] ph  /\  x  =  u ) ).
13 simpl 443 . . . . . . . 8  |-  ( ( [ v  /  y ] ph  /\  x  =  u )  ->  [ v  /  y ] ph )
1412, 13e1_ 28704 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  [ v  /  y ] ph ).
15 simpr 447 . . . . . . . 8  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
163, 15e1_ 28704 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  y  =  v ).
17 pm3.2 434 . . . . . . 7  |-  ( [ v  /  y ]
ph  ->  ( y  =  v  ->  ( [
v  /  y ]
ph  /\  y  =  v ) ) )
1814, 16, 17e11 28765 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ v  / 
y ] ph  /\  y  =  v ) ).
19 sbequ2 1640 . . . . . . 7  |-  ( y  =  v  ->  ( [ v  /  y ] ph  ->  ph ) )
2019imdistanri 672 . . . . . 6  |-  ( ( [ v  /  y ] ph  /\  y  =  v )  ->  ( ph  /\  y  =  v ) )
2118, 20e1_ 28704 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ph  /\  y  =  v ) ).
22 simpl 443 . . . . 5  |-  ( (
ph  /\  y  =  v )  ->  ph )
2321, 22e1_ 28704 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ph ).
24 pm3.2 434 . . . 4  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ph  ->  (
( x  =  u  /\  y  =  v )  /\  ph )
) )
253, 23, 24e11 28765 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
2625in1 28638 . 2  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
27 idn1 28641 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
28 simpl 443 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( x  =  u  /\  y  =  v ) )
2927, 28e1_ 28704 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( x  =  u  /\  y  =  v ) ).
3029, 4e1_ 28704 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  x  =  u ).
3129, 15e1_ 28704 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  y  =  v ).
32 simpr 447 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ph )
3327, 32e1_ 28704 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ph ).
34 pm3.21 435 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  ( ph  /\  y  =  v )
) )
3531, 33, 34e11 28765 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  (
ph  /\  y  =  v ) ).
36 sbequ1 1871 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  [ v  / 
y ] ph )
)
3736imdistanri 672 . . . . . . . . 9  |-  ( (
ph  /\  y  =  v )  ->  ( [ v  /  y ] ph  /\  y  =  v ) )
3835, 37e1_ 28704 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ v  /  y ] ph  /\  y  =  v ) ).
39 simpl 443 . . . . . . . 8  |-  ( ( [ v  /  y ] ph  /\  y  =  v )  ->  [ v  /  y ] ph )
4038, 39e1_ 28704 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ v  /  y ]
ph ).
41 pm3.21 435 . . . . . . 7  |-  ( x  =  u  ->  ( [ v  /  y ] ph  ->  ( [
v  /  y ]
ph  /\  x  =  u ) ) )
4230, 40, 41e11 28765 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ v  /  y ] ph  /\  x  =  u ) ).
43 sbequ1 1871 . . . . . . 7  |-  ( x  =  u  ->  ( [ v  /  y ] ph  ->  [ u  /  x ] [ v  /  y ] ph ) )
4443imdistanri 672 . . . . . 6  |-  ( ( [ v  /  y ] ph  /\  x  =  u )  ->  ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u ) )
4542, 44e1_ 28704 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ).
46 simpl 443 . . . . 5  |-  ( ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u )  ->  [ u  /  x ] [ v  /  y ] ph )
4745, 46e1_ 28704 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ u  /  x ] [ v  /  y ] ph ).
48 pm3.2 434 . . . 4  |-  ( ( x  =  u  /\  y  =  v )  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ) )
4929, 47, 48e11 28765 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ).
5049in1 28638 . 2  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) )
5126, 50impbii 180 1  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1632   [wsb 1638
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-vd1 28637
  Copyright terms: Public domain W3C validator