Step | Hyp | Ref
| Expression |
1 | | ax-1 5 |
. . . . . . 7
⊢ (ψ → (φ → ψ)) |
2 | 1 | a1i 9 |
. . . . . 6
⊢ (φ → (ψ → (φ → ψ))) |
3 | 2 | sbimi 1644 |
. . . . . . 7
⊢
([y / x]φ →
[y / x](ψ →
(φ → ψ))) |
4 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎxφ |
5 | 4 | sbf 1657 |
. . . . . . 7
⊢
([y / x]φ ↔
φ) |
6 | | sbim 1824 |
. . . . . . 7
⊢
([y / x](ψ →
(φ → ψ)) ↔ ([y / x]ψ → [y / x](φ → ψ))) |
7 | 3, 5, 6 | 3imtr3i 189 |
. . . . . 6
⊢ (φ → ([y / x]ψ → [y / x](φ → ψ))) |
8 | 2, 7 | anim12d 318 |
. . . . 5
⊢ (φ → ((ψ ∧
[y / x]ψ) →
((φ → ψ) ∧
[y / x](φ →
ψ)))) |
9 | 8 | imim1d 69 |
. . . 4
⊢ (φ → ((((φ → ψ) ∧
[y / x](φ →
ψ)) → x = y) →
((ψ ∧
[y / x]ψ) →
x = y))) |
10 | 9 | 2alimdv 1758 |
. . 3
⊢ (φ → (∀x∀y(((φ → ψ) ∧
[y / x](φ →
ψ)) → x = y) →
∀x∀y((ψ ∧
[y / x]ψ) →
x = y))) |
11 | | ax-17 1416 |
. . . 4
⊢ ((φ → ψ) → ∀y(φ → ψ)) |
12 | 11 | mo3h 1950 |
. . 3
⊢ (∃*x(φ → ψ) ↔ ∀x∀y(((φ → ψ) ∧
[y / x](φ →
ψ)) → x = y)) |
13 | | ax-17 1416 |
. . . 4
⊢ (ψ → ∀yψ) |
14 | 13 | mo3h 1950 |
. . 3
⊢ (∃*xψ ↔ ∀x∀y((ψ ∧
[y / x]ψ) →
x = y)) |
15 | 10, 12, 14 | 3imtr4g 194 |
. 2
⊢ (φ → (∃*x(φ → ψ) → ∃*xψ)) |
16 | 15 | com12 27 |
1
⊢ (∃*x(φ → ψ) → (φ → ∃*xψ)) |