Theorem 19.41rgVD 33435

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

1::	|- ( ps -> ( ph -> ( ph /\ ps ) ) )
2:1:	|- ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
3:2:	|- A. x ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
4:3:	|- ( A. x ( ps -> A. x ps ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) )
5::	|- (. A. x ( ps -> A. x ps ) ->. A. x ( ps -> A. x ps ) ).
6:4,5:	|- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) ).
7::	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ps ).
8:6,7:	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ( ph -> ( ph /\ ps ) ) ).
9:8:	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. ( E. x ph -> E. x ( ph /\ ps ) ) ).
10:9:	|- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
11:5:	|- (. A. x ( ps -> A. x ps ) ->. ( ps -> A. x ps ) ).
12:10,11:	|- (. A. x ( ps -> A. x ps ) ->. ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
13:12:	|- (. A. x ( ps -> A. x ps ) ->. ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) ).
14:13:	|- (. A. x ( ps -> A. x ps ) ->. ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) ).
qed:14:	|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

Assertion

Ref	Expression
19.41rgVD	|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

Proof of Theorem 19.41rgVD

Step	Hyp	Ref	Expression
1		idn1 33084	. . . . . . . . 9 |- (. A. x ( ps -> A. x ps ) ->. A. x ( ps -> A. x ps ) ).
2		pm3.2 447	. . . . . . . . . . . . 13 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
3	2	com12 31	. . . . . . . . . . . 12 |- ( ps -> ( ph -> ( ph /\ ps ) ) )
4	3	a1i 11	. . . . . . . . . . 11 |- ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
5	4	ax-gen 1605	. . . . . . . . . 10 |- A. x ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
6		al2im 1622	. . . . . . . . . 10 |- ( A. x ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) ) -> ( A. x ( ps -> A. x ps ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) ) )
7	5, 6	e0a 33302	. . . . . . . . 9 |- ( A. x ( ps -> A. x ps ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) )
8	1, 7	e1a 33146	. . . . . . . 8 |- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) ).
9		idn2 33132	. . . . . . . 8 |- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ps ).
10		id 22	. . . . . . . 8 |- ( ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) )
11	8, 9, 10	e12 33254	. . . . . . 7 |- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ( ph -> ( ph /\ ps ) ) ).
12		exim 1641	. . . . . . 7 |- ( A. x ( ph -> ( ph /\ ps ) ) -> ( E. x ph -> E. x ( ph /\ ps ) ) )
13	11, 12	e2 33150	. . . . . 6 |- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. ( E. x ph -> E. x ( ph /\ ps ) ) ).
14	13	in2 33124	. . . . 5 |- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
15		sp 1845	. . . . . 6 |- ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
16	1, 15	e1a 33146	. . . . 5 |- (. A. x ( ps -> A. x ps ) ->. ( ps -> A. x ps ) ).
17		imim2 53	. . . . 5 |- ( ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) -> ( ( ps -> A. x ps ) -> ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ) )
18	14, 16, 17	e11 33207	. . . 4 |- (. A. x ( ps -> A. x ps ) ->. ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
19		pm2.04 82	. . . 4 |- ( ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) -> ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) )
20	18, 19	e1a 33146	. . 3 |- (. A. x ( ps -> A. x ps ) ->. ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) ).
21		pm3.31 445	. . 3 |- ( ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )
22	20, 21	e1a 33146	. 2 |- (. A. x ( ps -> A. x ps ) ->. ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) ).
23	22	in1 33081	1 |- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1381   E.wex 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-vd1 33080  df-vd2 33088

This theorem is referenced by: (None)