Proof of Theorem 19.41rgVD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | idn1 44599 | . . . . . . . . 9
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   ) | 
| 2 |  | pm3.2 469 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | 
| 3 | 2 | com12 32 | . . . . . . . . . . . 12
⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | 
| 4 | 3 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) | 
| 5 | 4 | ax-gen 1794 | . . . . . . . . . 10
⊢
∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) | 
| 6 |  | al2im 1813 | . . . . . . . . . 10
⊢
(∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) → (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))) | 
| 7 | 5, 6 | e0a 44797 | . . . . . . . . 9
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))) | 
| 8 | 1, 7 | e1a 44652 | . . . . . . . 8
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))   ) | 
| 9 |  | idn2 44638 | . . . . . . . 8
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥𝜓   ) | 
| 10 |  | id 22 | . . . . . . . 8
⊢
((∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))) | 
| 11 | 8, 9, 10 | e12 44749 | . . . . . . 7
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))   ) | 
| 12 |  | exim 1833 | . . . . . . 7
⊢
(∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) | 
| 13 | 11, 12 | e2 44656 | . . . . . 6
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ,   ∀𝑥𝜓   ▶   (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))   ) | 
| 14 | 13 | in2 44630 | . . . . 5
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   ) | 
| 15 |  | sp 2182 | . . . . . 6
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓)) | 
| 16 | 1, 15 | e1a 44652 | . . . . 5
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → ∀𝑥𝜓)   ) | 
| 17 |  | imim2 58 | . . . . 5
⊢
((∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → ((𝜓 → ∀𝑥𝜓) → (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))))) | 
| 18 | 14, 16, 17 | e11 44713 | . . . 4
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))   ) | 
| 19 |  | pm2.04 90 | . . . 4
⊢ ((𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))) | 
| 20 | 18, 19 | e1a 44652 | . . 3
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))   ) | 
| 21 |  | pm3.31 449 | . . 3
⊢
((∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) | 
| 22 | 20, 21 | e1a 44652 | . 2
⊢ (   ∀𝑥(𝜓 → ∀𝑥𝜓)   ▶   ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))   ) | 
| 23 | 22 | in1 44596 | 1
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) |