Theorem hbimpgVD 34105

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

Assertion

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

Proof of Theorem hbimpgVD

Step	Hyp	Ref	Expression
1		hba1 1901	. . . 4 |- ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
2		hba1 1901	. . . 4 |- ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
3	1, 2	hban 1936	. . 3 |- ( ( 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 33793	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. -. ph ).
5		idn1 33745	. . . . . . . . . . 11 |- (. ( 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 455	. . . . . . . . . . 11 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ph -> A. x ph ) )
7	5, 6	e1a 33807	. . . . . . . . . 10 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
8		hbntal 33720	. . . . . . . . . 10 |- ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
9	7, 8	e1a 33807	. . . . . . . . 9 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
10		sp 1864	. . . . . . . . 9 |- ( A. x ( -. ph -> A. x -. ph ) -> ( -. ph -> A. x -. ph ) )
11	9, 10	e1a 33807	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
12		pm2.27 39	. . . . . . . 8 |- ( -. ph -> ( ( -. ph -> A. x -. ph ) -> A. x -. ph ) )
13	4, 11, 12	e21 33921	. . . . . . 7 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x -. ph ).
14		pm2.21 108	. . . . . . . 8 |- ( -. ph -> ( ph -> ps ) )
15	14	alimi 1638	. . . . . . 7 |- ( A. x -. ph -> A. x ( ph -> ps ) )
16	13, 15	e2 33811	. . . . . 6 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x ( ph -> ps ) ).
17	16	in2 33785	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
18		simpr 459	. . . . . . . 8 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ps -> A. x ps ) )
19	5, 18	e1a 33807	. . . . . . 7 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
20		sp 1864	. . . . . . 7 |- ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
21	19, 20	e1a 33807	. . . . . 6 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ps ) ).
22		ax-1 6	. . . . . . 7 |- ( ps -> ( ph -> ps ) )
23	22	alimi 1638	. . . . . 6 |- ( A. x ps -> A. x ( ph -> ps ) )
24		imim1 76	. . . . . 6 |- ( ( ps -> A. x ps ) -> ( ( A. x ps -> A. x ( ph -> ps ) ) -> ( ps -> A. x ( ph -> ps ) ) ) )
25	21, 23, 24	e10 33874	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
26		jao 510	. . . . 5 |- ( ( -. ph -> A. x ( ph -> ps ) ) -> ( ( ps -> A. x ( ph -> ps ) ) -> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
27	17, 25, 26	e11 33868	. . . 4 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
28		imor 410	. . . 4 |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
29		imbi1 321	. . . . 5 |- ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ( ph -> ps ) -> A. x ( ph -> ps ) ) <-> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
30	29	biimprcd 225	. . . 4 |- ( ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) -> ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
31	27, 28, 30	e10 33874	. . 3 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
32	3, 31	gen11nv 33797	. 2 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
33	32	in1 33742	1 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 366   /\ wa 367   A.wal 1396

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-12 1859

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-vd1 33741  df-vd2 33749

This theorem is referenced by: (None)