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

Theorem hbexgVD 28360
Description: Virtual deduction proof of hbexg 27987. 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 27987 is hbexgVD 28360 without virtual deductions and was automatically derived from hbexgVD 28360. (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 1794 . . 3  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x A. x A. y ( ph  ->  A. x ph ) )
2 hba1 1794 . . . . 5  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y A. y A. x ( ph  ->  A. x ph ) )
3 alcom 1744 . . . . 5  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y A. x (
ph  ->  A. x ph )
)
43albii 1572 . . . . 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 28007 . . . . . . . . . . . . . . . . 17  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y (
ph  ->  A. x ph ) ).
7 ax-7 1741 . . . . . . . . . . . . . . . . 17  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y A. x
( ph  ->  A. x ph ) )
86, 7e1_ 28070 . . . . . . . . . . . . . . . 16  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x (
ph  ->  A. x ph ) ).
9 sp 1755 . . . . . . . . . . . . . . . 16  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x ( ph  ->  A. x ph )
)
108, 9e1_ 28070 . . . . . . . . . . . . . . 15  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( ph  ->  A. x ph ) ).
11 hbntal 27984 . . . . . . . . . . . . . . 15  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
1210, 11e1_ 28070 . . . . . . . . . . . . . 14  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
135, 12gen11nv 28060 . . . . . . . . . . . . 13  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y A. x ( -.  ph  ->  A. x  -.  ph ) ).
14 ax-7 1741 . . . . . . . . . . . . 13  |-  ( A. y A. x ( -. 
ph  ->  A. x  -.  ph )  ->  A. x A. y
( -.  ph  ->  A. x  -.  ph )
)
1513, 14e1_ 28070 . . . . . . . . . . . 12  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( -.  ph  ->  A. x  -.  ph ) ).
16 sp 1755 . . . . . . . . . . . 12  |-  ( A. x A. y ( -. 
ph  ->  A. x  -.  ph )  ->  A. y ( -. 
ph  ->  A. x  -.  ph ) )
1715, 16e1_ 28070 . . . . . . . . . . 11  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( -.  ph  ->  A. x  -.  ph ) ).
18 hbalg 27986 . . . . . . . . . . 11  |-  ( A. y ( -.  ph  ->  A. x  -.  ph )  ->  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )
)
1917, 18e1_ 28070 . . . . . . . . . 10  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
20 sp 1755 . . . . . . . . . 10  |-  ( A. y ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  ( A. y  -. 
ph  ->  A. x A. y  -.  ph ) )
2119, 20e1_ 28070 . . . . . . . . 9  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
221, 21gen11nv 28060 . . . . . . . 8  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph ) ).
23 hbntal 27984 . . . . . . . 8  |-  ( A. x ( A. y  -.  ph  ->  A. x A. y  -.  ph )  ->  A. x ( -. 
A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2422, 23e1_ 28070 . . . . . . 7  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) ).
25 sp 1755 . . . . . . 7  |-  ( A. x ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph )  ->  ( -.  A. y  -.  ph  ->  A. x  -.  A. y  -.  ph ) )
2624, 25e1_ 28070 . . . . . 6  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y  -. 
ph  ->  A. x  -.  A. y  -.  ph ) ).
27 df-ex 1548 . . . . . 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 28137 . . . . 5  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x  -.  A. y  -.  ph ) ).
3127albii 1572 . . . . 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 28137 . . . 4  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E. y ph  ->  A. x E. y ph ) ).
355, 34gen11nv 28060 . . 3  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y ( E. y ph  ->  A. x E. y ph ) ).
361, 35gen11nv 28060 . 2  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x A. y ( E. y ph  ->  A. x E. y ph ) ).
3736in1 28004 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 1546   E.wex 1547
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-vd1 28003
  Copyright terms: Public domain W3C validator