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

Theorem hbexgVD 28682
Description: Virtual deduction proof of hbexg 28322. 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. hbexg 28322 is hbexgVD 28682 without virtual deductions and was automatically derived from hbexgVD 28682. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( ph  ->  A. x ph ) ).
2:1:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  A. x ( ph  ->  A. x ph ) ).
3:2:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( ph  ->  A. x ph ) ).
4:3:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( -.  ph  ->  A. x -.  ph ) ).
5::  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y  A. x ( ph  ->  A. x ph ) )
6::  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y  A. y A. x ( ph  ->  A. x ph ) )
7:5:  |-  ( A. y A. x A. y ( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
8:5,6,7:  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y  A. x A. y ( ph  ->  A. x ph ) )
9:8,4:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  A. x ( -.  ph  ->  A. x -.  ph ) ).
10:9:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( -.  ph  ->  A. x -.  ph ) ).
11:10:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( -.  ph  ->  A. x -.  ph ) ).
12:11:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( A. y -.  ph  ->  A. x A. y -.  ph ) ).
13:12:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A.  y -.  ph  ->  A. x A. y -.  ph ) ).
14::  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x  A. x A. y ( ph  ->  A. x ph ) )
15:13,14:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( A. y -.  ph  ->  A. x A. y -.  ph ) ).
16:15:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( -.  A. y -.  ph  ->  A. x -.  A. y -.  ph ) ).
17:16:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y -.  ph  ->  A. x -.  A. y -.  ph ) ).
18::  |-  ( E. y ph  <->  -.  A. y -.  ph )
19:17,18:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E.  y ph  ->  A. x -.  A. y -.  ph ) ).
20:18:  |-  ( A. x E. y ph  <->  A. x -.  A. y -.  ph )
21:19,20:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E.  y ph  ->  A. x E. y ph ) ).
22:8,21:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( E. y ph  ->  A. x E. y ph ) ).
23:14,22:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( E. y ph  ->  A. x E. y ph ) ).
qed:23:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( E. y ph  ->  A. x E. y ph ) ).
Assertion
Ref Expression
hbexgVD  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. y
( E. y ph  ->  A. x E. y ph ) )

Proof of Theorem hbexgVD
StepHypRef Expression
1 hba1 1719 . . 3  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. x A. y ( ph  ->  A. x ph ) )
2 hba1 1719 . . . . 5  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y A. y A. x ( ph  ->  A. x ph ) )
3 alcom 1711 . . . . 5  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y A. x (
ph  ->  A. x ph )
)
43albii 1553 . . . . 5  |-  ( A. y A. x A. y
( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
52, 3, 43imtr4i 257 . . . 4  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x A. y ( ph  ->  A. x ph ) )
6 idn1 28342 . . . . . . . . . . . . . . . . 17  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y (
ph  ->  A. x ph ) ).
7 ax-7 1708 . . . . . . . . . . . . . . . . 17  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x
( ph  ->  A. x ph ) )
86, 7e1_ 28399 . . . . . . . . . . . . . . . 16  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x (
ph  ->  A. x ph ) ).
9 sp 1716 . . . . . . . . . . . . . . . 16  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x ( ph  ->  A. x ph )
)
108, 9e1_ 28399 . . . . . . . . . . . . . . 15  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( ph  ->  A. x ph ) ).
11 hbntal 28319 . . . . . . . . . . . . . . 15  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
1210, 11e1_ 28399 . . . . . . . . . . . . . 14  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
135, 12gen11nv 28389 . . . . . . . . . . . . 13  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x ( -.  ph  ->  A. x  -.  ph ) ).
14 ax-7 1708 . . . . . . . . . . . . 13  |-  ( A. y A. x ( -. 
ph  ->  A. x  -.  ph )  ->  A. x A. y
( -.  ph  ->  A. x  -.  ph )
)
1513, 14e1_ 28399 . . . . . . . . . . . 12  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( -.  ph  ->  A. x  -.  ph ) ).
16 sp 1716 . . . . . . . . . . . 12  |-  ( A. x A. y ( -. 
ph  ->  A. x  -.  ph )  ->  A. y ( -. 
ph  ->  A. x  -.  ph ) )
1715, 16e1_ 28399 . . . . . . . . . . 11  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( -.  ph  ->  A. x  -.  ph ) ).
18 hbalg 28321 . . . . . . . . . . 11  |-  ( A. y ( -.  ph  ->  A. x  -.  ph )  ->  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )
)
1917, 18e1_ 28399 . . . . . . . . . 10  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
20 sp 1716 . . . . . . . . . 10  |-  ( A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  ( A. y  -. 
ph  ->  A. x A. y  -.  ph ) )
2119, 20e1_ 28399 . . . . . . . . 9  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
221, 21gen11nv 28389 . . . . . . . 8  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
23 hbntal 28319 . . . . . . . 8  |-  ( A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  A. x ( -. 
A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2422, 23e1_ 28399 . . . . . . 7  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ).
25 sp 1716 . . . . . . 7  |-  ( A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph )  ->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2624, 25e1_ 28399 . . . . . 6  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph ) ).
27 df-ex 1529 . . . . . 6  |-  ( E. y ph  <->  -.  A. y  -.  ph )
28 imbi1 313 . . . . . . 7  |-  ( ( E. y ph  <->  -.  A. y  -.  ph )  ->  (
( E. y ph  ->  A. x  -.  A. y  -.  ph )  <->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ) )
2928biimprcd 216 . . . . . 6  |-  ( ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph )  -> 
( ( E. y ph 
<->  -.  A. y  -. 
ph )  ->  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ) )
3026, 27, 29e10 28467 . . . . 5  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ).
3127albii 1553 . . . . 5  |-  ( A. x E. y ph  <->  A. x  -.  A. y  -.  ph )
32 imbi2 314 . . . . . 6  |-  ( ( A. x E. y ph 
<-> 
A. x  -.  A. y  -.  ph )  -> 
( ( E. y ph  ->  A. x E. y ph )  <->  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ) )
3332biimprcd 216 . . . . 5  |-  ( ( E. y ph  ->  A. x  -.  A. y  -.  ph )  ->  (
( A. x E. y ph  <->  A. x  -.  A. y  -.  ph )  -> 
( E. y ph  ->  A. x E. y ph ) ) )
3430, 31, 33e10 28467 . . . 4  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x E. y ph ) ).
355, 34gen11nv 28389 . . 3  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( E. y ph  ->  A. x E. y ph ) ).
361, 35gen11nv 28389 . 2  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( E. y ph  ->  A. x E. y ph ) ).
3736in1 28339 1  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. y
( E. y ph  ->  A. x E. y ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176   A.wal 1527   E.wex 1528
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
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532  df-vd1 28338
  Copyright terms: Public domain W3C validator