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

Theorem hbexgVD 36943
Description: Virtual deduction proof of hbexg 36560. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. hbexg 36560 is hbexgVD 36943 without virtual deductions and was automatically derived from hbexgVD 36943. (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 1953 . . 3  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. x A. y ( ph  ->  A. x ph ) )
2 hba1 1953 . . . . 5  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y A. y A. x ( ph  ->  A. x ph ) )
3 alcom 1897 . . . . 5  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y A. x (
ph  ->  A. x ph )
)
43albii 1687 . . . . 5  |-  ( A. y A. x A. y
( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
52, 3, 43imtr4i 269 . . . 4  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x A. y ( ph  ->  A. x ph ) )
6 idn1 36582 . . . . . . . . . . . . . . . . 17  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y (
ph  ->  A. x ph ) ).
7 ax-11 1894 . . . . . . . . . . . . . . . . 17  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x
( ph  ->  A. x ph ) )
86, 7e1a 36644 . . . . . . . . . . . . . . . 16  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x (
ph  ->  A. x ph ) ).
9 sp 1912 . . . . . . . . . . . . . . . 16  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x ( ph  ->  A. x ph )
)
108, 9e1a 36644 . . . . . . . . . . . . . . 15  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( ph  ->  A. x ph ) ).
11 hbntal 36557 . . . . . . . . . . . . . . 15  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
1210, 11e1a 36644 . . . . . . . . . . . . . 14  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
135, 12gen11nv 36634 . . . . . . . . . . . . 13  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x ( -.  ph  ->  A. x  -.  ph ) ).
14 ax-11 1894 . . . . . . . . . . . . 13  |-  ( A. y A. x ( -. 
ph  ->  A. x  -.  ph )  ->  A. x A. y
( -.  ph  ->  A. x  -.  ph )
)
1513, 14e1a 36644 . . . . . . . . . . . 12  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( -.  ph  ->  A. x  -.  ph ) ).
16 sp 1912 . . . . . . . . . . . 12  |-  ( A. x A. y ( -. 
ph  ->  A. x  -.  ph )  ->  A. y ( -. 
ph  ->  A. x  -.  ph ) )
1715, 16e1a 36644 . . . . . . . . . . 11  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( -.  ph  ->  A. x  -.  ph ) ).
18 hbalg 36559 . . . . . . . . . . 11  |-  ( A. y ( -.  ph  ->  A. x  -.  ph )  ->  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )
)
1917, 18e1a 36644 . . . . . . . . . 10  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
20 sp 1912 . . . . . . . . . 10  |-  ( A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  ( A. y  -. 
ph  ->  A. x A. y  -.  ph ) )
2119, 20e1a 36644 . . . . . . . . 9  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
221, 21gen11nv 36634 . . . . . . . 8  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
23 hbntal 36557 . . . . . . . 8  |-  ( A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  A. x ( -. 
A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2422, 23e1a 36644 . . . . . . 7  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ).
25 sp 1912 . . . . . . 7  |-  ( A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph )  ->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2624, 25e1a 36644 . . . . . 6  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph ) ).
27 df-ex 1660 . . . . . 6  |-  ( E. y ph  <->  -.  A. y  -.  ph )
28 imbi1 324 . . . . . . 7  |-  ( ( E. y ph  <->  -.  A. y  -.  ph )  ->  (
( E. y ph  ->  A. x  -.  A. y  -.  ph )  <->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ) )
2928biimprcd 228 . . . . . 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 36711 . . . . 5  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ).
3127albii 1687 . . . . 5  |-  ( A. x E. y ph  <->  A. x  -.  A. y  -.  ph )
32 imbi2 325 . . . . . 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 228 . . . . 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 36711 . . . 4  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x E. y ph ) ).
355, 34gen11nv 36634 . . 3  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( E. y ph  ->  A. x E. y ph ) ).
361, 35gen11nv 36634 . 2  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( E. y ph  ->  A. x E. y ph ) ).
3736in1 36579 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187   A.wal 1435   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664  df-vd1 36578
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator