Proof of Theorem 19.41rgVD
Step | Hyp | Ref
| Expression |
1 | | idn1 42194 |
. . . . . . . . 9
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ ∀𝑥(𝜓 → ∀𝑥𝜓) ) |
2 | | pm3.2 470 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
3 | 2 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) |
5 | 4 | ax-gen 1798 |
. . . . . . . . . 10
⊢
∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) |
6 | | al2im 1817 |
. . . . . . . . . 10
⊢
(∀𝑥((𝜓 → ∀𝑥𝜓) → (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))) → (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))))) |
7 | 5, 6 | e0a 42392 |
. . . . . . . . 9
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))) |
8 | 1, 7 | e1a 42247 |
. . . . . . . 8
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) ) |
9 | | idn2 42233 |
. . . . . . . 8
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) , ∀𝑥𝜓 ▶ ∀𝑥𝜓 ) |
10 | | id 22 |
. . . . . . . 8
⊢
((∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓))) → (∀𝑥𝜓 → ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)))) |
11 | 8, 9, 10 | e12 42344 |
. . . . . . 7
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) , ∀𝑥𝜓 ▶ ∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) ) |
12 | | exim 1836 |
. . . . . . 7
⊢
(∀𝑥(𝜑 → (𝜑 ∧ 𝜓)) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
13 | 11, 12 | e2 42251 |
. . . . . 6
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) , ∀𝑥𝜓 ▶ (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) ) |
14 | 13 | in2 42225 |
. . . . 5
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ (∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) ) |
15 | | sp 2176 |
. . . . . 6
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓)) |
16 | 1, 15 | e1a 42247 |
. . . . 5
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ (𝜓 → ∀𝑥𝜓) ) |
17 | | imim2 58 |
. . . . 5
⊢
((∀𝑥𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → ((𝜓 → ∀𝑥𝜓) → (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))))) |
18 | 14, 16, 17 | e11 42308 |
. . . 4
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) ) |
19 | | pm2.04 90 |
. . . 4
⊢ ((𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) → (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))) |
20 | 18, 19 | e1a 42247 |
. . 3
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ (∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) ) |
21 | | pm3.31 450 |
. . 3
⊢
((∃𝑥𝜑 → (𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) |
22 | 20, 21 | e1a 42247 |
. 2
⊢ ( ∀𝑥(𝜓 → ∀𝑥𝜓) ▶ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) ) |
23 | 22 | in1 42191 |
1
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) |