Proof of Theorem hbimpg
Step | Hyp | Ref
| Expression |
1 | | hba1 2137 |
. . 3
⊢
(∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥(𝜑 → ∀𝑥𝜑)) |
2 | | hba1 2137 |
. . 3
⊢
(∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥∀𝑥(𝜓 → ∀𝑥𝜓)) |
3 | 1, 2 | hban 2113 |
. 2
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))) |
4 | | hbntal 37790 |
. . . . . 6
⊢
(∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)) |
5 | 4 | adantr 480 |
. . . . 5
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)) |
6 | 5 | 19.21bi 2047 |
. . . 4
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) |
7 | | pm2.21 119 |
. . . . 5
⊢ (¬
𝜑 → (𝜑 → 𝜓)) |
8 | 7 | alimi 1730 |
. . . 4
⊢
(∀𝑥 ¬
𝜑 → ∀𝑥(𝜑 → 𝜓)) |
9 | 6, 8 | syl6 34 |
. . 3
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → (¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))) |
10 | | simpr 476 |
. . . . 5
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓)) |
11 | 10 | 19.21bi 2047 |
. . . 4
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → (𝜓 → ∀𝑥𝜓)) |
12 | | ax-1 6 |
. . . . 5
⊢ (𝜓 → (𝜑 → 𝜓)) |
13 | 12 | alimi 1730 |
. . . 4
⊢
(∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓)) |
14 | 11, 13 | syl6 34 |
. . 3
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → (𝜓 → ∀𝑥(𝜑 → 𝜓))) |
15 | 9, 14 | jad 173 |
. 2
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))) |
16 | 3, 15 | alrimih 1741 |
1
⊢
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))) |