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

Theorem hbexgVD 28919
Description: Virtual deduction proof of hbexg 28544. 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 28544 is hbexgVD 28919 without virtual deductions and was automatically derived from hbexgVD 28919. (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 1804 . . 3  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. x A. y ( ph  ->  A. x ph ) )
2 hba1 1804 . . . . 5  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y A. y A. x ( ph  ->  A. x ph ) )
3 alcom 1752 . . . . 5  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y A. x (
ph  ->  A. x ph )
)
43albii 1575 . . . . 5  |-  ( A. y A. x A. y
( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
52, 3, 43imtr4i 258 . . . 4  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x A. y ( ph  ->  A. x ph ) )
6 idn1 28566 . . . . . . . . . . . . . . . . 17  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y (
ph  ->  A. x ph ) ).
7 ax-7 1749 . . . . . . . . . . . . . . . . 17  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x
( ph  ->  A. x ph ) )
86, 7e1_ 28629 . . . . . . . . . . . . . . . 16  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x (
ph  ->  A. x ph ) ).
9 sp 1763 . . . . . . . . . . . . . . . 16  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x ( ph  ->  A. x ph )
)
108, 9e1_ 28629 . . . . . . . . . . . . . . 15  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( ph  ->  A. x ph ) ).
11 hbntal 28541 . . . . . . . . . . . . . . 15  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
1210, 11e1_ 28629 . . . . . . . . . . . . . 14  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
135, 12gen11nv 28619 . . . . . . . . . . . . 13  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x ( -.  ph  ->  A. x  -.  ph ) ).
14 ax-7 1749 . . . . . . . . . . . . 13  |-  ( A. y A. x ( -. 
ph  ->  A. x  -.  ph )  ->  A. x A. y
( -.  ph  ->  A. x  -.  ph )
)
1513, 14e1_ 28629 . . . . . . . . . . . 12  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( -.  ph  ->  A. x  -.  ph ) ).
16 sp 1763 . . . . . . . . . . . 12  |-  ( A. x A. y ( -. 
ph  ->  A. x  -.  ph )  ->  A. y ( -. 
ph  ->  A. x  -.  ph ) )
1715, 16e1_ 28629 . . . . . . . . . . 11  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( -.  ph  ->  A. x  -.  ph ) ).
18 hbalg 28543 . . . . . . . . . . 11  |-  ( A. y ( -.  ph  ->  A. x  -.  ph )  ->  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )
)
1917, 18e1_ 28629 . . . . . . . . . 10  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
20 sp 1763 . . . . . . . . . 10  |-  ( A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  ( A. y  -. 
ph  ->  A. x A. y  -.  ph ) )
2119, 20e1_ 28629 . . . . . . . . 9  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
221, 21gen11nv 28619 . . . . . . . 8  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
23 hbntal 28541 . . . . . . . 8  |-  ( A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  A. x ( -. 
A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2422, 23e1_ 28629 . . . . . . 7  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ).
25 sp 1763 . . . . . . 7  |-  ( A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph )  ->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2624, 25e1_ 28629 . . . . . 6  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph ) ).
27 df-ex 1551 . . . . . 6  |-  ( E. y ph  <->  -.  A. y  -.  ph )
28 imbi1 314 . . . . . . 7  |-  ( ( E. y ph  <->  -.  A. y  -.  ph )  ->  (
( E. y ph  ->  A. x  -.  A. y  -.  ph )  <->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ) )
2928biimprcd 217 . . . . . 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 28696 . . . . 5  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ).
3127albii 1575 . . . . 5  |-  ( A. x E. y ph  <->  A. x  -.  A. y  -.  ph )
32 imbi2 315 . . . . . 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 217 . . . . 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 28696 . . . 4  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x E. y ph ) ).
355, 34gen11nv 28619 . . 3  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( E. y ph  ->  A. x E. y ph ) ).
361, 35gen11nv 28619 . 2  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( E. y ph  ->  A. x E. y ph ) ).
3736in1 28563 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 177   A.wal 1549   E.wex 1550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-vd1 28562
  Copyright terms: Public domain W3C validator