Theorem hbimpgVD 37280

Description: Virtual deduction proof of hbimpg 36897. 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 36897 is hbimpgVD 37280 without virtual deductions and was automatically derived from hbimpgVD 37280. (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 1956	. . . 4 |- ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
2		hba1 1956	. . . 4 |- ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
3	1, 2	hban 1992	. . 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 36969	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. -. ph ).
5		idn1 36921	. . . . . . . . . . 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 459	. . . . . . . . . . 11 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ph -> A. x ph ) )
7	5, 6	e1a 36983	. . . . . . . . . 10 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
8		hbntal 36896	. . . . . . . . . 10 |- ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
9	7, 8	e1a 36983	. . . . . . . . 9 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
10		sp 1915	. . . . . . . . 9 |- ( A. x ( -. ph -> A. x -. ph ) -> ( -. ph -> A. x -. ph ) )
11	9, 10	e1a 36983	. . . . . . . 8 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
12		pm2.27 41	. . . . . . . 8 |- ( -. ph -> ( ( -. ph -> A. x -. ph ) -> A. x -. ph ) )
13	4, 11, 12	e21 37096	. . . . . . 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 1679	. . . . . . 7 |- ( A. x -. ph -> A. x ( ph -> ps ) )
16	13, 15	e2 36987	. . . . . 6 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ,. -. ph ->. A. x ( ph -> ps ) ).
17	16	in2 36961	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
18		simpr 463	. . . . . . . 8 |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ps -> A. x ps ) )
19	5, 18	e1a 36983	. . . . . . 7 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
20		sp 1915	. . . . . . 7 |- ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
21	19, 20	e1a 36983	. . . . . 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 1679	. . . . . 6 |- ( A. x ps -> A. x ( ph -> ps ) )
24		imim1 80	. . . . . 6 |- ( ( ps -> A. x ps ) -> ( ( A. x ps -> A. x ( ph -> ps ) ) -> ( ps -> A. x ( ph -> ps ) ) ) )
25	21, 23, 24	e10 37050	. . . . 5 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
26		jao 515	. . . . 5 |- ( ( -. ph -> A. x ( ph -> ps ) ) -> ( ( ps -> A. x ( ph -> ps ) ) -> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
27	17, 25, 26	e11 37044	. . . 4 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
28		imor 414	. . . 4 |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
29		imbi1 325	. . . . 5 |- ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ( ph -> ps ) -> A. x ( ph -> ps ) ) <-> ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ) )
30	29	biimprcd 229	. . . 4 |- ( ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) -> ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
31	27, 28, 30	e10 37050	. . 3 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
32	3, 31	gen11nv 36973	. 2 |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
33	32	in1 36918	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 188   \/ wo 370   /\ wa 371   A.wal 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-12 1910

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1659  df-nf 1663  df-vd1 36917  df-vd2 36925

This theorem is referenced by: (None)