Proof of Theorem sbi1
Step | Hyp | Ref
| Expression |
1 | | sbequ2 1869 |
. . . . 5
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) |
2 | | sbequ2 1869 |
. . . . 5
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → (𝜑 → 𝜓))) |
3 | 1, 2 | syl5d 71 |
. . . 4
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))) |
4 | | sbequ1 2096 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝜓 → [𝑦 / 𝑥]𝜓)) |
5 | 3, 4 | syl6d 73 |
. . 3
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))) |
6 | 5 | sps 2043 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))) |
7 | | sb4 2344 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
8 | | sb4 2344 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))) |
9 | | ax-2 7 |
. . . . . 6
⊢ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜓))) |
10 | 9 | al2imi 1733 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜓))) |
11 | | sb2 2340 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜓) → [𝑦 / 𝑥]𝜓) |
12 | 10, 11 | syl6 34 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜓)) |
13 | 8, 12 | syl6 34 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜓))) |
14 | 7, 13 | syl5d 71 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))) |
15 | 6, 14 | pm2.61i 175 |
1
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |