Theorem 19.41rgVD 41608

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

1::	⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
2:1:	⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → ( 𝜑 ∧ 𝜓))))
3:2:	⊢ ∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
4:3:	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
5::	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
6:4,5:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))   )
7::	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶    ∀𝑥𝜓   )
8:6,7:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶    ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))   )
9:8:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶    (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))   )
10:9:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
11:5:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ∀ 𝑥𝜓)   )
12:10,11:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ( ∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
13:12:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))   )
14:13:	⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ((∃𝑥 𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))   )
qed:14:	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Assertion

Ref	Expression
19.41rgVD	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Proof of Theorem 19.41rgVD

Step	Hyp	Ref	Expression
1		idn1 41280	. . . . . . . . 9 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
2		pm3.2 473	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
3	2	com12 32	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
4	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
5	4	ax-gen 1797	. . . . . . . . . 10 ⊢ ∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
6		al2im 1816	. . . . . . . . . 10 ⊢ (∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) → (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))))
7	5, 6	e0a 41478	. . . . . . . . 9 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
8	1, 7	e1a 41333	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))   )
9		idn2 41319	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥𝜓   )
10		id 22	. . . . . . . 8 ⊢ ((∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
11	8, 9, 10	e12 41430	. . . . . . 7 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))   )
12		exim 1835	. . . . . . 7 ⊢ (∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
13	11, 12	e2 41337	. . . . . 6 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))   )
14	13	in2 41311	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
15		sp 2180	. . . . . 6 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
16	1, 15	e1a 41333	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ∀𝑥𝜓)   )
17		imim2 58	. . . . 5 ⊢ ((∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → ((𝜓 → ∀𝑥𝜓) → (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))))
18	14, 16, 17	e11 41394	. . . 4 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
19		pm2.04 90	. . . 4 ⊢ ((𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))))
20	18, 19	e1a 41333	. . 3 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))   )
21		pm3.31 453	. . 3 ⊢ ((∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))
22	20, 21	e1a 41333	. 2 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))   )
23	22	in1 41277	1 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-vd1 41276  df-vd2 41284

This theorem is referenced by: (None)