Proof of Theorem hbimdOLD
Step | Hyp | Ref
| Expression |
1 | | hbimd.1 |
. . . . 5
⊢ (φ → ∀xφ) |
2 | | hbimd.2 |
. . . . 5
⊢ (φ → (ψ → ∀xψ)) |
3 | 1, 2 | alrimih 1565 |
. . . 4
⊢ (φ → ∀x(ψ → ∀xψ)) |
4 | | sp 1747 |
. . . . . 6
⊢ (∀xψ → ψ) |
5 | | hbn1 1730 |
. . . . . 6
⊢ (¬ ∀xψ → ∀x ¬
∀xψ) |
6 | 4, 5 | nsyl4 134 |
. . . . 5
⊢ (¬ ∀x ¬
∀xψ → ψ) |
7 | 6 | con1i 121 |
. . . 4
⊢ (¬ ψ → ∀x ¬
∀xψ) |
8 | | con3 126 |
. . . . 5
⊢ ((ψ → ∀xψ) → (¬ ∀xψ → ¬ ψ)) |
9 | 8 | al2imi 1561 |
. . . 4
⊢ (∀x(ψ → ∀xψ) → (∀x ¬
∀xψ → ∀x ¬
ψ)) |
10 | 3, 7, 9 | syl2im 34 |
. . 3
⊢ (φ → (¬ ψ → ∀x ¬
ψ)) |
11 | | pm2.21 100 |
. . . 4
⊢ (¬ ψ → (ψ → χ)) |
12 | 11 | alimi 1559 |
. . 3
⊢ (∀x ¬
ψ → ∀x(ψ → χ)) |
13 | 10, 12 | syl6 29 |
. 2
⊢ (φ → (¬ ψ → ∀x(ψ → χ))) |
14 | | hbimd.3 |
. . 3
⊢ (φ → (χ → ∀xχ)) |
15 | | ax-1 5 |
. . . 4
⊢ (χ → (ψ → χ)) |
16 | 15 | alimi 1559 |
. . 3
⊢ (∀xχ → ∀x(ψ → χ)) |
17 | 14, 16 | syl6 29 |
. 2
⊢ (φ → (χ → ∀x(ψ → χ))) |
18 | 13, 17 | jad 154 |
1
⊢ (φ → ((ψ → χ) → ∀x(ψ → χ))) |