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

Theorem 2pm13.193VD 29189
Description: Virtual deduction proof of 2pm13.193 28811. 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 28811 is 2pm13.193VD 29189 without virtual deductions and was automatically derived from 2pm13.193VD 29189. (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 28837 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) ).
2 simpl 445 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( x  =  u  /\  y  =  v ) )
31, 2e1_ 28900 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( x  =  u  /\  y  =  v ) ).
4 simpl 445 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
53, 4e1_ 28900 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  x  =  u ).
6 simpr 449 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  [ u  /  x ] [ v  / 
y ] ph )
71, 6e1_ 28900 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  [ u  /  x ] [ v  /  y ] ph ).
8 pm3.21 437 . . . . . . . . . 10  |-  ( x  =  u  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  ( [
u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ) )
95, 7, 8e11 28961 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ u  /  x ] [ v  / 
y ] ph  /\  x  =  u ) ).
10 sbequ2 1662 . . . . . . . . . 10  |-  ( x  =  u  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  [ v  /  y ] ph ) )
1110imdistanri 674 . . . . . . . . 9  |-  ( ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u )  ->  ( [ v  /  y ] ph  /\  x  =  u ) )
129, 11e1_ 28900 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ v  / 
y ] ph  /\  x  =  u ) ).
13 simpl 445 . . . . . . . 8  |-  ( ( [ v  /  y ] ph  /\  x  =  u )  ->  [ v  /  y ] ph )
1412, 13e1_ 28900 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  [ v  /  y ] ph ).
15 simpr 449 . . . . . . . 8  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
163, 15e1_ 28900 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  y  =  v ).
17 pm3.2 436 . . . . . . 7  |-  ( [ v  /  y ]
ph  ->  ( y  =  v  ->  ( [
v  /  y ]
ph  /\  y  =  v ) ) )
1814, 16, 17e11 28961 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( [ v  / 
y ] ph  /\  y  =  v ) ).
19 sbequ2 1662 . . . . . . 7  |-  ( y  =  v  ->  ( [ v  /  y ] ph  ->  ph ) )
2019imdistanri 674 . . . . . 6  |-  ( ( [ v  /  y ] ph  /\  y  =  v )  ->  ( ph  /\  y  =  v ) )
2118, 20e1_ 28900 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ph  /\  y  =  v ) ).
22 simpl 445 . . . . 5  |-  ( (
ph  /\  y  =  v )  ->  ph )
2321, 22e1_ 28900 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ph ).
24 pm3.2 436 . . . 4  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ph  ->  (
( x  =  u  /\  y  =  v )  /\  ph )
) )
253, 23, 24e11 28961 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
2625in1 28834 . 2  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
27 idn1 28837 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
28 simpl 445 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( x  =  u  /\  y  =  v ) )
2927, 28e1_ 28900 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( x  =  u  /\  y  =  v ) ).
3029, 4e1_ 28900 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  x  =  u ).
3129, 15e1_ 28900 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  y  =  v ).
32 simpr 449 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ph )
3327, 32e1_ 28900 . . . . . . . . . 10  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ph ).
34 pm3.21 437 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  ( ph  /\  y  =  v )
) )
3531, 33, 34e11 28961 . . . . . . . . 9  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  (
ph  /\  y  =  v ) ).
36 sbequ1 1947 . . . . . . . . . 10  |-  ( y  =  v  ->  ( ph  ->  [ v  / 
y ] ph )
)
3736imdistanri 674 . . . . . . . . 9  |-  ( (
ph  /\  y  =  v )  ->  ( [ v  /  y ] ph  /\  y  =  v ) )
3835, 37e1_ 28900 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ v  /  y ] ph  /\  y  =  v ) ).
39 simpl 445 . . . . . . . 8  |-  ( ( [ v  /  y ] ph  /\  y  =  v )  ->  [ v  /  y ] ph )
4038, 39e1_ 28900 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ v  /  y ]
ph ).
41 pm3.21 437 . . . . . . 7  |-  ( x  =  u  ->  ( [ v  /  y ] ph  ->  ( [
v  /  y ]
ph  /\  x  =  u ) ) )
4230, 40, 41e11 28961 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ v  /  y ] ph  /\  x  =  u ) ).
43 sbequ1 1947 . . . . . . 7  |-  ( x  =  u  ->  ( [ v  /  y ] ph  ->  [ u  /  x ] [ v  /  y ] ph ) )
4443imdistanri 674 . . . . . 6  |-  ( ( [ v  /  y ] ph  /\  x  =  u )  ->  ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u ) )
4542, 44e1_ 28900 . . . . 5  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ).
46 simpl 445 . . . . 5  |-  ( ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u )  ->  [ u  /  x ] [ v  /  y ] ph )
4745, 46e1_ 28900 . . . 4  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ u  /  x ] [ v  /  y ] ph ).
48 pm3.2 436 . . . 4  |-  ( ( x  =  u  /\  y  =  v )  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ) )
4929, 47, 48e11 28961 . . 3  |-  (. (
( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ).
5049in1 28834 . 2  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) )
5126, 50impbii 182 1  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1654   [wsb 1660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1661  df-vd1 28833
  Copyright terms: Public domain W3C validator