Theorem 19.41rgVD 45495

Description: Virtual deduction proof of 19.41rg 45144. 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 45144 is 19.41rgVD 45495 without virtual deductions and was automatically derived from 19.41rgVD 45495. (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 45168	. . . . . . . . 9 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
2		pm3.2 474	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
3	2	com12 33	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
4	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
5	4	ax-gen 1822	. . . . . . . . . 10 ⊢ ∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))))
6		al2im 1841	. . . . . . . . . 10 ⊢ (∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) → (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))))
7	5, 6	e0a 45365	. . . . . . . . 9 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
8	1, 7	e1a 45221	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))   )
9		idn2 45207	. . . . . . . 8 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥𝜓   )
10		id 23	. . . . . . . 8 ⊢ ((∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))
11	8, 9, 10	e12 45317	. . . . . . 7 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))   )
12		exim 1861	. . . . . . 7 ⊢ (∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
13	11, 12	e2 45225	. . . . . 6 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))   )
14	13	in2 45199	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
15		sp 2225	. . . . . 6 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
16	1, 15	e1a 45221	. . . . 5 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ∀𝑥𝜓)   )
17		imim2 59	. . . . 5 ⊢ ((∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → ((𝜓 → ∀𝑥𝜓) → (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))))
18	14, 16, 17	e11 45282	. . . 4 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   )
19		pm2.04 91	. . . 4 ⊢ ((𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))))
20	18, 19	e1a 45221	. . 3 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))   )
21		pm3.31 454	. . 3 ⊢ ((∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))
22	20, 21	e1a 45221	. 2 ⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))   )
23	22	in1 45165	1 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-vd1 45164  df-vd2 45172

This theorem is referenced by: (None)