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

Theorem 2uasbanhVD 28687
Description: The following User's Proof is a Virtual Deduction proof (see: wvd1 28337) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 28327 is 2uasbanhVD 28687 without virtual deductions and was automatically derived from 2uasbanhVD 28687. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
h1::  |-  ( ch  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
100:1:  |-  ( ch  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
2:100:  |-  (. ch  ->.  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
3:2:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
4:3:  |-  (. ch  ->.  E. x E. y ( x  =  u  /\  y  =  v  ) ).
5:4:  |-  (. ch  ->.  ( -.  A. x x  =  y  \/  u  =  v )  ).
6:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) ).
7:3,6:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ph ).
8:2:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ).
9:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ps  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
10:8,9:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ps ).
101::  |-  ( [ v  /  y ] ( ph  /\  ps )  <->  ( [ v  /  y ] ph  /\  [ v  /  y ] ps ) )
102:101:  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  [ u  /  x ] ( [ v  /  y ] ph  /\  [ v  /  y ] ps ) )
103::  |-  ( [ u  /  x ] ( [ v  /  y ] ph  /\  [ v  /  y  ] ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\  [ u  /  x ] [ v  /  y ] ps ) )
104:102,103:  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\  [ u  /  x ] [ v  /  y ] ps ) )
11:7,10,104:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ( ph  /\  ps ) ).
110:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ) ).
12:11,110:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ).
120:12:  |-  ( ch  ->  E. x E. y ( ( x  =  u  /\  y  =  v  )  /\  ( ph  /\  ps ) ) )
13:1,120:  |-  ( ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) )
14::  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ).
15:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( x  =  u  /\  y  =  v ) ).
16:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ph  /\  ps ) ).
17:16:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ph ).
18:15,17:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
19:18:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
20:19:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) )  ->  E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
21:20:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
22:16:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ps ).
23:15,22:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ps ) ).
24:23:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->  ( ( x  =  u  /\  y  =  v )  /\  ps ) )
25:24:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) )  ->  E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )
26:25:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )
27:21,26:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y (  ( x  =  u  /\  y  =  v )  /\  ps ) ) )
qed:13,27:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y (  ( x  =  u  /\  y  =  v )  /\  ps ) ) )
Hypothesis
Ref Expression
2uasbanhVD.1  |-  ( ch  <->  ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
Assertion
Ref Expression
2uasbanhVD  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
Distinct variable groups:    x, u    y, u    x, v    y,
v
Allowed substitution hints:    ph( x, y, v, u)    ps( x, y, v, u)    ch( x, y, v, u)

Proof of Theorem 2uasbanhVD
StepHypRef Expression
1 idn1 28342 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ( (
x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ).
2 simpl 443 . . . . . . . 8  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  -> 
( x  =  u  /\  y  =  v ) )
31, 2e1_ 28399 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ( x  =  u  /\  y  =  v ) ).
4 simpr 447 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  -> 
( ph  /\  ps )
)
51, 4e1_ 28399 . . . . . . . 8  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ( ph  /\ 
ps ) ).
6 simpl 443 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ph )
75, 6e1_ 28399 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ph ).
8 pm3.2 434 . . . . . . 7  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ph  ->  (
( x  =  u  /\  y  =  v )  /\  ph )
) )
93, 7, 8e11 28460 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ( (
x  =  u  /\  y  =  v )  /\  ph ) ).
109in1 28339 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  -> 
( ( x  =  u  /\  y  =  v )  /\  ph ) )
1110eximi 1563 . . . 4  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
)  ->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
1211eximi 1563 . . 3  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )
)
13 simpr 447 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ps )
145, 13e1_ 28399 . . . . . . 7  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ps ).
15 pm3.2 434 . . . . . . 7  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ps  ->  (
( x  =  u  /\  y  =  v )  /\  ps )
) )
163, 14, 15e11 28460 . . . . . 6  |-  (. (
( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->.  ( (
x  =  u  /\  y  =  v )  /\  ps ) ).
1716in1 28339 . . . . 5  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  -> 
( ( x  =  u  /\  y  =  v )  /\  ps ) )
1817eximi 1563 . . . 4  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
)  ->  E. y
( ( x  =  u  /\  y  =  v )  /\  ps ) )
1918eximi 1563 . . 3  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps )
)
2012, 19jca 518 . 2  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  -> 
( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
21 2uasbanhVD.1 . . 3  |-  ( ch  <->  ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
2221biimpi 186 . . . . . . . . 9  |-  ( ch 
->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
2322dfvd1ir 28341 . . . . . . . 8  |-  (. ch  ->.  ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
24 simpl 443 . . . . . . . 8  |-  ( ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
2523, 24e1_ 28399 . . . . . . 7  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
26 simpl 443 . . . . . . . . . . 11  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( x  =  u  /\  y  =  v ) )
27262eximi 1564 . . . . . . . . . 10  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  E. x E. y
( x  =  u  /\  y  =  v ) )
2825, 27e1_ 28399 . . . . . . . . 9  |-  (. ch  ->.  E. x E. y ( x  =  u  /\  y  =  v ) ).
29 a9e2ndeq 28325 . . . . . . . . . 10  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
3029biimpri 197 . . . . . . . . 9  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
)
3128, 30e1_ 28399 . . . . . . . 8  |-  (. ch  ->.  ( -.  A. x  x  =  y  \/  u  =  v ) ).
32 2sb5nd 28326 . . . . . . . 8  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  -> 
( [ u  /  x ] [ v  / 
y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
3331, 32e1_ 28399 . . . . . . 7  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) ) ).
34 bi2 189 . . . . . . . 8  |-  ( ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  [ u  /  x ] [ v  /  y ] ph ) )
3534com12 27 . . . . . . 7  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )
)  ->  [ u  /  x ] [ v  /  y ] ph ) )
3625, 33, 35e11 28460 . . . . . 6  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ph ).
37 simpr 447 . . . . . . . 8  |-  ( ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )
3823, 37e1_ 28399 . . . . . . 7  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ).
39 2sb5nd 28326 . . . . . . . 8  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  -> 
( [ u  /  x ] [ v  / 
y ] ps  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
4031, 39e1_ 28399 . . . . . . 7  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ps  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
41 bi2 189 . . . . . . . 8  |-  ( ( [ u  /  x ] [ v  /  y ] ps  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps )  ->  [ u  /  x ] [ v  /  y ] ps ) )
4241com12 27 . . . . . . 7  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps )  ->  ( ( [ u  /  x ] [ v  /  y ] ps  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps )
)  ->  [ u  /  x ] [ v  /  y ] ps ) )
4338, 40, 42e11 28460 . . . . . 6  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ps ).
44 sban 2009 . . . . . . . 8  |-  ( [ v  /  y ] ( ph  /\  ps ) 
<->  ( [ v  / 
y ] ph  /\  [ v  /  y ] ps ) )
4544sbbii 1634 . . . . . . 7  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  [ u  /  x ] ( [ v  /  y ] ph  /\ 
[ v  /  y ] ps ) )
46 sban 2009 . . . . . . 7  |-  ( [ u  /  x ]
( [ v  / 
y ] ph  /\  [ v  /  y ] ps )  <->  ( [
u  /  x ] [ v  /  y ] ph  /\  [ u  /  x ] [ v  /  y ] ps ) )
4745, 46bitri 240 . . . . . 6  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\ 
[ u  /  x ] [ v  /  y ] ps ) )
48 simplbi2comg 1363 . . . . . . 7  |-  ( ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\ 
[ u  /  x ] [ v  /  y ] ps ) )  -> 
( [ u  /  x ] [ v  / 
y ] ps  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  [ u  /  x ] [ v  /  y ] (
ph  /\  ps )
) ) )
4948com13 74 . . . . . 6  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  ( [
u  /  x ] [ v  /  y ] ps  ->  ( ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\ 
[ u  /  x ] [ v  /  y ] ps ) )  ->  [ u  /  x ] [ v  /  y ] ( ph  /\  ps ) ) ) )
5036, 43, 47, 49e110 28448 . . . . 5  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ( ph  /\  ps ) ).
51 2sb5nd 28326 . . . . . 6  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  -> 
( [ u  /  x ] [ v  / 
y ] ( ph  /\ 
ps )  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
) ) )
5231, 51e1_ 28399 . . . . 5  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ) ).
53 bi1 178 . . . . . 6  |-  ( ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) )  ->  ( [
u  /  x ] [ v  /  y ] ( ph  /\  ps )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
) ) )
5453com12 27 . . . . 5  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  ->  ( ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
) ) )
5550, 52, 54e11 28460 . . . 4  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) ) ).
5655in1 28339 . . 3  |-  ( ch 
->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) )
5721, 56sylbir 204 . 2  |-  ( ( E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps )
) )
5820, 57impbii 180 1  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\ 
ps ) )  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1527   E.wex 1528    = 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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-fal 1311  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ne 2448  df-v 2790  df-vd1 28338
  Copyright terms: Public domain W3C validator