Proof of Theorem bj-nfimt
Step | Hyp | Ref
| Expression |
1 | | 19.35 1794 |
. . 3
⊢
(∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) |
2 | | df-nf 1701 |
. . . . . . 7
⊢
(Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) |
3 | 2 | biimpi 205 |
. . . . . 6
⊢
(Ⅎ𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) |
4 | 3 | imim1d 80 |
. . . . 5
⊢
(Ⅎ𝑥𝜑 → ((∀𝑥𝜑 → ∃𝑥𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))) |
5 | | df-nf 1701 |
. . . . . . 7
⊢
(Ⅎ𝑥𝜓 ↔ (∃𝑥𝜓 → ∀𝑥𝜓)) |
6 | 5 | biimpi 205 |
. . . . . 6
⊢
(Ⅎ𝑥𝜓 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
7 | 6 | imim2d 55 |
. . . . 5
⊢
(Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∃𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) |
8 | 4, 7 | syl9 75 |
. . . 4
⊢
(Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → ((∀𝑥𝜑 → ∃𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))) |
9 | | 19.38 1757 |
. . . 4
⊢
((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) |
10 | 8, 9 | syl8 74 |
. . 3
⊢
(Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → ((∀𝑥𝜑 → ∃𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)))) |
11 | 1, 10 | syl7bi 244 |
. 2
⊢
(Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))) |
12 | | df-nf 1701 |
. 2
⊢
(Ⅎ𝑥(𝜑 → 𝜓) ↔ (∃𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))) |
13 | 11, 12 | syl6ibr 241 |
1
⊢
(Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓))) |