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

Theorem hbexgVD 34107
Description: Virtual deduction proof of hbexg 33723. 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 33723 is hbexgVD 34107 without virtual deductions and was automatically derived from hbexgVD 34107. (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 1901 . . 3  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. x A. y ( ph  ->  A. x ph ) )
2 hba1 1901 . . . . 5  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y A. y A. x ( ph  ->  A. x ph ) )
3 alcom 1850 . . . . 5  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y A. x (
ph  ->  A. x ph )
)
43albii 1645 . . . . 5  |-  ( A. y A. x A. y
( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
52, 3, 43imtr4i 266 . . . 4  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x A. y ( ph  ->  A. x ph ) )
6 idn1 33745 . . . . . . . . . . . . . . . . 17  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y (
ph  ->  A. x ph ) ).
7 ax-11 1847 . . . . . . . . . . . . . . . . 17  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x
( ph  ->  A. x ph ) )
86, 7e1a 33807 . . . . . . . . . . . . . . . 16  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x (
ph  ->  A. x ph ) ).
9 sp 1864 . . . . . . . . . . . . . . . 16  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x ( ph  ->  A. x ph )
)
108, 9e1a 33807 . . . . . . . . . . . . . . 15  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( ph  ->  A. x ph ) ).
11 hbntal 33720 . . . . . . . . . . . . . . 15  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
1210, 11e1a 33807 . . . . . . . . . . . . . 14  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
135, 12gen11nv 33797 . . . . . . . . . . . . 13  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x ( -.  ph  ->  A. x  -.  ph ) ).
14 ax-11 1847 . . . . . . . . . . . . 13  |-  ( A. y A. x ( -. 
ph  ->  A. x  -.  ph )  ->  A. x A. y
( -.  ph  ->  A. x  -.  ph )
)
1513, 14e1a 33807 . . . . . . . . . . . 12  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( -.  ph  ->  A. x  -.  ph ) ).
16 sp 1864 . . . . . . . . . . . 12  |-  ( A. x A. y ( -. 
ph  ->  A. x  -.  ph )  ->  A. y ( -. 
ph  ->  A. x  -.  ph ) )
1715, 16e1a 33807 . . . . . . . . . . 11  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( -.  ph  ->  A. x  -.  ph ) ).
18 hbalg 33722 . . . . . . . . . . 11  |-  ( A. y ( -.  ph  ->  A. x  -.  ph )  ->  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )
)
1917, 18e1a 33807 . . . . . . . . . 10  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
20 sp 1864 . . . . . . . . . 10  |-  ( A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  ( A. y  -. 
ph  ->  A. x A. y  -.  ph ) )
2119, 20e1a 33807 . . . . . . . . 9  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
221, 21gen11nv 33797 . . . . . . . 8  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
23 hbntal 33720 . . . . . . . 8  |-  ( A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  A. x ( -. 
A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2422, 23e1a 33807 . . . . . . 7  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ).
25 sp 1864 . . . . . . 7  |-  ( A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph )  ->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2624, 25e1a 33807 . . . . . 6  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph ) ).
27 df-ex 1618 . . . . . 6  |-  ( E. y ph  <->  -.  A. y  -.  ph )
28 imbi1 321 . . . . . . 7  |-  ( ( E. y ph  <->  -.  A. y  -.  ph )  ->  (
( E. y ph  ->  A. x  -.  A. y  -.  ph )  <->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ) )
2928biimprcd 225 . . . . . 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 33874 . . . . 5  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ).
3127albii 1645 . . . . 5  |-  ( A. x E. y ph  <->  A. x  -.  A. y  -.  ph )
32 imbi2 322 . . . . . 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 225 . . . . 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 33874 . . . 4  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x E. y ph ) ).
355, 34gen11nv 33797 . . 3  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( E. y ph  ->  A. x E. y ph ) ).
361, 35gen11nv 33797 . 2  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( E. y ph  ->  A. x E. y ph ) ).
3736in1 33742 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 184   A.wal 1396   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-vd1 33741
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator