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

Theorem 2pm13.193VD 28679
Description: Virtual deduction proof of 2pm13.193 28318. 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 28318 is 2pm13.193VD 28679 without virtual deductions and was automatically derived from 2pm13.193VD 28679. (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 28342 . . . . 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_ 28399 . . . 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_ 28399 . . . . . . . . . 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_ 28399 . . . . . . . . . 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 28460 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ u  /  x ] [ v  / 
y ] ph  /\  x  =  u ) ).
10 sbequ2 1631 . . . . . . . . . 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_ 28399 . . . . . . . 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_ 28399 . . . . . . 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_ 28399 . . . . . . 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 28460 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ v  / 
y ] ph  /\  y  =  v ) ).
19 sbequ2 1631 . . . . . . 7  |-  ( y  =  v  ->  ( [ v  /  y ] ph  ->  ph ) )
2019imdistanri 672 . . . . . 6  |-  ( ( [ v  /  y ] ph  /\  y  =  v )  ->  ( ph  /\  y  =  v ) )
2118, 20e1_ 28399 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ph  /\  y  =  v ) ).
22 simpl 443 . . . . 5  |-  ( (
ph  /\  y  =  v )  ->  ph )
2321, 22e1_ 28399 . . . 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 28460 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
2625in1 28339 . 2  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
27 idn1 28342 . . . . 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_ 28399 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( x  =  u  /\  y  =  v ) ).
3029, 4e1_ 28399 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  x  =  u ).
3129, 15e1_ 28399 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  y  =  v ).
32 simpr 447 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ph )
3327, 32e1_ 28399 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ph ).
34 pm3.21 435 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  ( ph  /\  y  =  v )
) )
3531, 33, 34e11 28460 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  (
ph  /\  y  =  v ) ).
36 sbequ1 1859 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  [ v  / 
y ] ph )
)
3736imdistanri 672 . . . . . . . . 9  |-  ( (
ph  /\  y  =  v )  ->  ( [ v  /  y ] ph  /\  y  =  v ) )
3835, 37e1_ 28399 . . . . . . . 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_ 28399 . . . . . . 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 28460 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ v  /  y ] ph  /\  x  =  u ) ).
43 sbequ1 1859 . . . . . . 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_ 28399 . . . . 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_ 28399 . . . 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 28460 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ).
5049in1 28339 . 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 1623   [wsb 1629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-vd1 28338
  Copyright terms: Public domain W3C validator