Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hbexgVD Structured version   Visualization version   Unicode version
Theorem hbexgVD 39142
Description: Virtual deduction proof of hbexg 38772. 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 38772 is hbexgVD 39142 without virtual deductions and was automatically derived from hbexgVD 39142. (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 2151 . . 3 |- ( A. x A. y ( ph -> A. x ph ) -> A. x A. x A. y ( ph -> A. x ph ) )
2 hba1 2151 . . . . 5 |- ( A. y A. x ( ph -> A. x ph ) -> A. y A. y A. x ( ph -> A. x ph ) )
3 alcom 2037 . . . . 5 |- ( A. x A. y ( ph -> A. x ph ) <-> A. y A. x ( ph -> A. x ph ) )
43albii 1747 . . . . 5 |- ( A. y A. x A. y ( ph -> A. x ph ) <-> A. y A. y A. x ( ph -> A. x ph ) )
52, 3, 43imtr4i 281 . . . 4 |- ( A. x A. y ( ph -> A. x ph ) -> A. y A. x A. y ( ph -> A. x ph ) )
6 idn1 38790 . . . . . . . . . . . . . . . . 17 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( ph -> A. x ph ) ).
7 ax-11 2034 . . . . . . . . . . . . . . . . 17 |- ( A. x A. y ( ph -> A. x ph ) -> A. y A. x ( ph -> A. x ph ) )
86, 7e1a 38852 . . . . . . . . . . . . . . . 16 |- (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( ph -> A. x ph ) ).
9 sp 2053 . . . . . . . . . . . . . . . 16 |- ( A. y A. x ( ph -> A. x ph ) -> A. x ( ph -> A. x ph ) )
108, 9e1a 38852 . . . . . . . . . . . . . . 15 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( ph -> A. x ph ) ).
11 hbntal 38769 . . . . . . . . . . . . . . 15 |- ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
1210, 11e1a 38852 . . . . . . . . . . . . . 14 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. ph -> A. x -. ph ) ).
135, 12gen11nv 38842 . . . . . . . . . . . . 13 |- (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( -. ph -> A. x -. ph ) ).
14 ax-11 2034 . . . . . . . . . . . . 13 |- ( A. y A. x ( -. ph -> A. x -. ph ) -> A. x A. y ( -. ph -> A. x -. ph ) )
1513, 14e1a 38852 . . . . . . . . . . . 12 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( -. ph -> A. x -. ph ) ).
16 sp 2053 . . . . . . . . . . . 12 |- ( A. x A. y ( -. ph -> A. x -. ph ) -> A. y ( -. ph -> A. x -. ph ) )
1715, 16e1a 38852 . . . . . . . . . . 11 |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( -. ph -> A. x -. ph ) ).
18 hbalg 38771 . . . . . . . . . . 11 |- ( A. y ( -. ph -> A. x -. ph ) -> A. y ( A. y -. ph -> A. x A. y -. ph ) )
1917, 18e1a 38852 . . . . . . . . . 10 |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( A. y -. ph -> A. x A. y -. ph ) ).
20 sp 2053 . . . . . . . . . 10 |- ( A. y ( A. y -. ph -> A. x A. y -. ph ) -> ( A. y -. ph -> A. x A. y -. ph ) )
2119, 20e1a 38852 . . . . . . . . 9 |- (. A. x A. y ( ph -> A. x ph ) ->. ( A. y -. ph -> A. x A. y -. ph ) ).
221, 21gen11nv 38842 . . . . . . . 8 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( A. y -. ph -> A. x A. y -. ph ) ).
23 hbntal 38769 . . . . . . . 8 |- ( A. x ( A. y -. ph -> A. x A. y -. ph ) -> A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) )
2422, 23e1a 38852 . . . . . . 7 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
25 sp 2053 . . . . . . 7 |- ( A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) -> ( -. A. y -. ph -> A. x -. A. y -. ph ) )
2624, 25e1a 38852 . . . . . 6 |- (. A. x A. y ( ph -> A. x ph ) ->. ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
27 df-ex 1705 . . . . . 6 |- ( E. y ph <-> -. A. y -. ph )
28 imbi1 337 . . . . . . 7 |- ( ( E. y ph <-> -. A. y -. ph ) -> ( ( E. y ph -> A. x -. A. y -. ph ) <-> ( -. A. y -. ph -> A. x -. A. y -. ph ) ) )
2928biimprcd 240 . . . . . 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 38919 . . . . 5 |- (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x -. A. y -. ph ) ).
3127albii 1747 . . . . 5 |- ( A. x E. y ph <-> A. x -. A. y -. ph )
32 imbi2 338 . . . . . 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 240 . . . . 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 38919 . . . 4 |- (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x E. y ph ) ).
355, 34gen11nv 38842 . . 3 |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( E. y ph -> A. x E. y ph ) ).
361, 35gen11nv 38842 . 2 |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( E. y ph -> A. x E. y ph ) ).
3736in1 38787 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 196   A.wal 1481   E.wex 1704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710  df-vd1 38786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator