Metamath Proof Explorer

Theorem hbexgVD

Description: Virtual deduction proof of hbexg . 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 is hbexgVD without virtual deductions and was automatically derived from hbexgVD . (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 ) ).

Ref Expression
Assertion hbexgVD 
|- ( A. x A. y ( ph -> A. x ph ) -> A. x A. y ( E. y ph -> A. x E. y ph ) )

Proof

Step Hyp Ref Expression
1 hba1 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. x A. x A. y ( ph -> A. x ph ) )
2 hba1 
 |-  ( A. y A. x ( ph -> A. x ph ) -> A. y A. y A. x ( ph -> A. x ph ) )
3 alcom 
 |-  ( A. x A. y ( ph -> A. x ph ) <-> A. y A. x ( ph -> A. x ph ) )
4 3 albii 
 |-  ( A. y A. x A. y ( ph -> A. x ph ) <-> A. y A. y A. x ( ph -> A. x ph ) )
5 2 3 4 3imtr4i 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. y A. x A. y ( ph -> A. x ph ) )
6 idn1 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( ph -> A. x ph ) ).
7 ax-11 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. y A. x ( ph -> A. x ph ) )
8 6 7 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( ph -> A. x ph ) ).
9 sp 
 |-  ( A. y A. x ( ph -> A. x ph ) -> A. x ( ph -> A. x ph ) )
10 8 9 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x ( ph -> A. x ph ) ).
11 hbntal 
 |-  ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
12 10 11 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. ph -> A. x -. ph ) ).
13 5 12 gen11nv 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( -. ph -> A. x -. ph ) ).
14 ax-11 
 |-  ( A. y A. x ( -. ph -> A. x -. ph ) -> A. x A. y ( -. ph -> A. x -. ph ) )
15 13 14 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( -. ph -> A. x -. ph ) ).
16 sp 
 |-  ( A. x A. y ( -. ph -> A. x -. ph ) -> A. y ( -. ph -> A. x -. ph ) )
17 15 16 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. y ( -. ph -> A. x -. ph ) ).
18 hbalg 
 |-  ( A. y ( -. ph -> A. x -. ph ) -> A. y ( A. y -. ph -> A. x A. y -. ph ) )
19 17 18 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. y ( A. y -. ph -> A. x A. y -. ph ) ).
20 sp 
 |-  ( A. y ( A. y -. ph -> A. x A. y -. ph ) -> ( A. y -. ph -> A. x A. y -. ph ) )
21 19 20 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. ( A. y -. ph -> A. x A. y -. ph ) ).
22 1 21 gen11nv 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x ( A. y -. ph -> A. x A. y -. ph ) ).
23 hbntal 
 |-  ( A. x ( A. y -. ph -> A. x A. y -. ph ) -> A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) )
24 22 23 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
25 sp 
 |-  ( A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) -> ( -. A. y -. ph -> A. x -. A. y -. ph ) )
26 24 25 e1a 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
27 df-ex 
 |-  ( E. y ph <-> -. A. y -. ph )
28 imbi1 
 |-  ( ( E. y ph <-> -. A. y -. ph ) -> ( ( E. y ph -> A. x -. A. y -. ph ) <-> ( -. A. y -. ph -> A. x -. A. y -. ph ) ) )
29 28 biimprcd 
 |-  ( ( -. A. y -. ph -> A. x -. A. y -. ph ) -> ( ( E. y ph <-> -. A. y -. ph ) -> ( E. y ph -> A. x -. A. y -. ph ) ) )
30 26 27 29 e10 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x -. A. y -. ph ) ).
31 27 albii 
 |-  ( A. x E. y ph <-> A. x -. A. y -. ph )
32 imbi2 
 |-  ( ( 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 ) ) )
33 32 biimprcd 
 |-  ( ( 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 ) ) )
34 30 31 33 e10 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x E. y ph ) ).
35 5 34 gen11nv 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. y ( E. y ph -> A. x E. y ph ) ).
36 1 35 gen11nv 
 |-  (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( E. y ph -> A. x E. y ph ) ).
37 36 in1 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. x A. y ( E. y ph -> A. x E. y ph ) )