Proof of Theorem nford
Step | Hyp | Ref
| Expression |
1 | | nford.1 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥𝜓) |
2 | | nford.2 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥𝜒) |
3 | | df-nf 1350 |
. . . . . . 7
⊢
(Ⅎ𝑥𝜓 ↔ ∀𝑥(𝜓 → ∀𝑥𝜓)) |
4 | | df-nf 1350 |
. . . . . . 7
⊢
(Ⅎ𝑥𝜒 ↔ ∀𝑥(𝜒 → ∀𝑥𝜒)) |
5 | 3, 4 | anbi12i 433 |
. . . . . 6
⊢
((Ⅎ𝑥𝜓 ∧ Ⅎ𝑥𝜒) ↔ (∀𝑥(𝜓 → ∀𝑥𝜓) ∧ ∀𝑥(𝜒 → ∀𝑥𝜒))) |
6 | 5 | biimpi 113 |
. . . . 5
⊢
((Ⅎ𝑥𝜓 ∧ Ⅎ𝑥𝜒) → (∀𝑥(𝜓 → ∀𝑥𝜓) ∧ ∀𝑥(𝜒 → ∀𝑥𝜒))) |
7 | 1, 2, 6 | syl2anc 391 |
. . . 4
⊢ (𝜑 → (∀𝑥(𝜓 → ∀𝑥𝜓) ∧ ∀𝑥(𝜒 → ∀𝑥𝜒))) |
8 | | 19.26 1370 |
. . . 4
⊢
(∀𝑥((𝜓 → ∀𝑥𝜓) ∧ (𝜒 → ∀𝑥𝜒)) ↔ (∀𝑥(𝜓 → ∀𝑥𝜓) ∧ ∀𝑥(𝜒 → ∀𝑥𝜒))) |
9 | 7, 8 | sylibr 137 |
. . 3
⊢ (𝜑 → ∀𝑥((𝜓 → ∀𝑥𝜓) ∧ (𝜒 → ∀𝑥𝜒))) |
10 | | orc 633 |
. . . . . . 7
⊢ (𝜓 → (𝜓 ∨ 𝜒)) |
11 | 10 | alimi 1344 |
. . . . . 6
⊢
(∀𝑥𝜓 → ∀𝑥(𝜓 ∨ 𝜒)) |
12 | 11 | imim2i 12 |
. . . . 5
⊢ ((𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥(𝜓 ∨ 𝜒))) |
13 | | olc 632 |
. . . . . . 7
⊢ (𝜒 → (𝜓 ∨ 𝜒)) |
14 | 13 | alimi 1344 |
. . . . . 6
⊢
(∀𝑥𝜒 → ∀𝑥(𝜓 ∨ 𝜒)) |
15 | 14 | imim2i 12 |
. . . . 5
⊢ ((𝜒 → ∀𝑥𝜒) → (𝜒 → ∀𝑥(𝜓 ∨ 𝜒))) |
16 | 12, 15 | jaao 639 |
. . . 4
⊢ (((𝜓 → ∀𝑥𝜓) ∧ (𝜒 → ∀𝑥𝜒)) → ((𝜓 ∨ 𝜒) → ∀𝑥(𝜓 ∨ 𝜒))) |
17 | 16 | alimi 1344 |
. . 3
⊢
(∀𝑥((𝜓 → ∀𝑥𝜓) ∧ (𝜒 → ∀𝑥𝜒)) → ∀𝑥((𝜓 ∨ 𝜒) → ∀𝑥(𝜓 ∨ 𝜒))) |
18 | 9, 17 | syl 14 |
. 2
⊢ (𝜑 → ∀𝑥((𝜓 ∨ 𝜒) → ∀𝑥(𝜓 ∨ 𝜒))) |
19 | | df-nf 1350 |
. 2
⊢
(Ⅎ𝑥(𝜓 ∨ 𝜒) ↔ ∀𝑥((𝜓 ∨ 𝜒) → ∀𝑥(𝜓 ∨ 𝜒))) |
20 | 18, 19 | sylibr 137 |
1
⊢ (𝜑 → Ⅎ𝑥(𝜓 ∨ 𝜒)) |