Metamath Proof Explorer

Theorem hbimpgVD

Description: Virtual deduction proof of hbimpg . 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. hbimpg is hbimpgVD without virtual deductions and was automatically derived from hbimpgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ).
2:1: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
3:: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. -. ph ).
4:2: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
5:4: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
6:3,5: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. A. x -. ph ).
7:: |- ( -. ph -> ( ph -> ps ) )
8:7: |- ( A. x -. ph -> A. x ( ph -> ps ) )
9:6,8: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. A. x ( ph -> ps ) ).
10:9: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
11:: |- ( ps -> ( ph -> ps ) )
12:11: |- ( A. x ps -> A. x ( ph -> ps ) )
13:1: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
14:13: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ps ) ).
15:14,12: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
16:10,15: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
17:: |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
18:16,17: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
19:: |- ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
20:: |- ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
21:19,20: |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) )
22:21,18: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
qed:22: |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )

Ref Expression
Assertion hbimpgVD 
|- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 hba1 
 |-  ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
2 hba1 
 |-  ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
3 1 2 hban 
 |-  ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) )
4 idn2 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. -. ph ).
5 idn1 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ).
6 simpl 
 |-  ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ph -> A. x ph ) )
7 5 6 e1a 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
8 hbntal 
 |-  ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
9 7 8 e1a 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
10 sp 
 |-  ( A. x ( -. ph -> A. x -. ph ) -> ( -. ph -> A. x -. ph ) )
11 9 10 e1a 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
12 pm2.27 
 |-  ( -. ph -> ( ( -. ph -> A. x -. ph ) -> A. x -. ph ) )
13 4 11 12 e21 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x -. ph ).
14 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
15 14 alimi 
 |-  ( A. x -. ph -> A. x ( ph -> ps ) )
16 13 15 e2 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x ( ph -> ps ) ).
17 16 in2 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
18 simpr 
 |-  ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ps -> A. x ps ) )
19 5 18 e1a 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
20 sp 
 |-  ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
21 19 20 e1a 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ps ) ).
22 ax-1 
 |-  ( ps -> ( ph -> ps ) )
23 22 alimi 
 |-  ( A. x ps -> A. x ( ph -> ps ) )
24 imim1 
 |-  ( ( ps -> A. x ps ) -> ( ( A. x ps -> A. x ( ph -> ps ) ) -> ( ps -> A. x ( ph -> ps ) ) ) )
25 21 23 24 e10 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
26 jao 
 |-  ( ( -. ph -> A. x ( ph -> ps ) ) -> ( ( ps -> A. x ( ph -> ps ) ) -> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
27 17 25 26 e11 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
28 imor 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
29 imbi1 
 |-  ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ( ph -> ps ) -> A. x ( ph -> ps ) ) <-> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
30 29 biimprcd 
 |-  ( ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) -> ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
31 27 28 30 e10 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
32 3 31 gen11nv 
 |-  (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
33 32 in1 
 |-  ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )