Theorem 19.41rgVD 45142

Description: Virtual deduction proof of 19.41rg 44791. 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 44791 is 19.41rgVD 45142 without virtual deductions and was automatically derived from 19.41rgVD 45142. (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 44815	. . . . . . . . 9 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
2		pm3.2 469	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
3	2	com12 32	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
4	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
5	4	ax-gen 1796	. . . . . . . . . 10 ⊢ ∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
6		al2im 1815	. . . . . . . . . 10 ⊢ (∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) → (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))))
7	5, 6	e0a 45012	. . . . . . . . 9 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
8	1, 7	e1a 44868	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))   )
9		idn2 44854	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥𝜓   )
10		id 22	. . . . . . . 8 ⊢ ((∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
11	8, 9, 10	e12 44964	. . . . . . 7 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))   )
12		exim 1835	. . . . . . 7 ⊢ (∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
13	11, 12	e2 44872	. . . . . 6 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))   )
14	13	in2 44846	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
15		sp 2190	. . . . . 6 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
16	1, 15	e1a 44868	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ∀𝑥𝜓)   )
17		imim2 58	. . . . 5 ⊢ ((∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → ((𝜓 → ∀𝑥𝜓) → (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))))
18	14, 16, 17	e11 44929	. . . 4 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
19		pm2.04 90	. . . 4 ⊢ ((𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))))
20	18, 19	e1a 44868	. . 3 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))   )
21		pm3.31 449	. . 3 ⊢ ((∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))
22	20, 21	e1a 44868	. 2 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))   )
23	22	in1 44812	1 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-vd1 44811  df-vd2 44819

This theorem is referenced by: (None)