Step | Hyp | Ref
| Expression |
1 | | ax-17 1416 |
. . . 4
⊢ ((φ ∧ ψ) → ∀y(φ ∧ ψ)) |
2 | | hbs1 1811 |
. . . . 5
⊢
([y / x]φ →
∀x[y / x]φ) |
3 | | hbs1 1811 |
. . . . 5
⊢
([y / x]ψ →
∀x[y / x]ψ) |
4 | 2, 3 | hban 1436 |
. . . 4
⊢
(([y / x]φ ∧ [y / x]ψ) →
∀x([y / x]φ ∧ [y / x]ψ)) |
5 | | sbequ12 1651 |
. . . . 5
⊢ (x = y →
(φ ↔ [y / x]φ)) |
6 | | sbequ12 1651 |
. . . . 5
⊢ (x = y →
(ψ ↔ [y / x]ψ)) |
7 | 5, 6 | anbi12d 442 |
. . . 4
⊢ (x = y →
((φ ∧
ψ) ↔ ([y / x]φ ∧
[y / x]ψ))) |
8 | 1, 4, 7 | cbvexh 1635 |
. . 3
⊢ (∃x(φ ∧ ψ) ↔ ∃y([y / x]φ ∧
[y / x]ψ)) |
9 | | ax-17 1416 |
. . . . . . 7
⊢ (φ → ∀yφ) |
10 | 9 | mo3h 1950 |
. . . . . 6
⊢ (∃*xφ ↔ ∀x∀y((φ ∧
[y / x]φ) →
x = y)) |
11 | | ax-4 1397 |
. . . . . . 7
⊢ (∀y((φ ∧
[y / x]φ) →
x = y)
→ ((φ ∧ [y / x]φ) →
x = y)) |
12 | 11 | sps 1427 |
. . . . . 6
⊢ (∀x∀y((φ ∧
[y / x]φ) →
x = y)
→ ((φ ∧ [y / x]φ) →
x = y)) |
13 | 10, 12 | sylbi 114 |
. . . . 5
⊢ (∃*xφ → ((φ ∧
[y / x]φ) →
x = y)) |
14 | | sbequ2 1649 |
. . . . . . . . 9
⊢ (x = y →
([y / x]ψ →
ψ)) |
15 | 14 | imim2i 12 |
. . . . . . . 8
⊢ (((φ ∧
[y / x]φ) →
x = y)
→ ((φ ∧ [y / x]φ) →
([y / x]ψ →
ψ))) |
16 | 15 | expd 245 |
. . . . . . 7
⊢ (((φ ∧
[y / x]φ) →
x = y)
→ (φ → ([y / x]φ → ([y / x]ψ → ψ)))) |
17 | 16 | com4t 79 |
. . . . . 6
⊢
([y / x]φ →
([y / x]ψ →
(((φ ∧
[y / x]φ) →
x = y)
→ (φ → ψ)))) |
18 | 17 | imp 115 |
. . . . 5
⊢
(([y / x]φ ∧ [y / x]ψ) →
(((φ ∧
[y / x]φ) →
x = y)
→ (φ → ψ))) |
19 | 13, 18 | syl5 28 |
. . . 4
⊢
(([y / x]φ ∧ [y / x]ψ) →
(∃*xφ →
(φ → ψ))) |
20 | 19 | exlimiv 1486 |
. . 3
⊢ (∃y([y / x]φ ∧
[y / x]ψ) →
(∃*xφ →
(φ → ψ))) |
21 | 8, 20 | sylbi 114 |
. 2
⊢ (∃x(φ ∧ ψ) → (∃*xφ → (φ → ψ))) |
22 | 21 | impcom 116 |
1
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ)) |