Theorem hbimpgVD 37341

Description: Virtual deduction proof of hbimpg 36965. 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 36965 is hbimpgVD 37341 without virtual deductions and was automatically derived from hbimpgVD 37341. (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 1989	. . . 4 |- ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
2		hba1 1989	. . . 4 |- ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
3	1, 2	hban 2025	. . 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 37035	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. -. ph ).
5		idn1 36987	. . . . . . . . . . 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 463	. . . . . . . . . . 11 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ph -> A. x ph ) )
7	5, 6	e1a 37049	. . . . . . . . . 10 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
8		hbntal 36964	. . . . . . . . . 10 |- ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
9	7, 8	e1a 37049	. . . . . . . . 9 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
10		sp 1948	. . . . . . . . 9 |- ( A. x ( -. ph -> A. x -. ph ) -> ( -. ph -> A. x -. ph ) )
11	9, 10	e1a 37049	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
12		pm2.27 40	. . . . . . . 8 |- ( -. ph -> ( ( -. ph -> A. x -. ph ) -> A. x -. ph ) )
13	4, 11, 12	e21 37157	. . . . . . 7 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x -. ph ).
14		pm2.21 112	. . . . . . . 8 |- ( -. ph -> ( ph -> ps ) )
15	14	alimi 1695	. . . . . . 7 |- ( A. x -. ph -> A. x ( ph -> ps ) )
16	13, 15	e2 37053	. . . . . 6 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x ( ph -> ps ) ).
17	16	in2 37027	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
18		simpr 467	. . . . . . . 8 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ps -> A. x ps ) )
19	5, 18	e1a 37049	. . . . . . 7 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
20		sp 1948	. . . . . . 7 |- ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
21	19, 20	e1a 37049	. . . . . 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 1695	. . . . . 6 |- ( A. x ps -> A. x ( ph -> ps ) )
24		imim1 79	. . . . . 6 |- ( ( ps -> A. x ps ) -> ( ( A. x ps -> A. x ( ph -> ps ) ) -> ( ps -> A. x ( ph -> ps ) ) ) )
25	21, 23, 24	e10 37116	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
26		jao 519	. . . . 5 |- ( ( -. ph -> A. x ( ph -> ps ) ) -> ( ( ps -> A. x ( ph -> ps ) ) -> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
27	17, 25, 26	e11 37110	. . . 4 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
28		imor 418	. . . 4 |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
29		imbi1 329	. . . . 5 |- ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ( ph -> ps ) -> A. x ( ph -> ps ) ) <-> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
30	29	biimprcd 233	. . . 4 |- ( ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) -> ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
31	27, 28, 30	e10 37116	. . 3 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
32	3, 31	gen11nv 37039	. 2 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
33	32	in1 36984	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 189   \/ wo 374   /\ wa 375   A.wal 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-vd1 36983  df-vd2 36991

This theorem is referenced by: (None)