| Step | Hyp | Ref
| Expression |
| 1 | | equequ1 2024 |
. . . . . 6
⊢ (𝑎 = 𝑡 → (𝑎 = 𝑏 ↔ 𝑡 = 𝑏)) |
| 2 | | neeq1 3003 |
. . . . . 6
⊢ (𝑎 = 𝑡 → (𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐)) |
| 3 | 1, 2 | 3anbi12d 1439 |
. . . . 5
⊢ (𝑎 = 𝑡 → ((𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
| 4 | 3 | 2exbidv 1924 |
. . . 4
⊢ (𝑎 = 𝑡 → (∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
| 5 | 4 | cbvexvw 2036 |
. . 3
⊢
(∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝑎 = 𝑡 → (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
| 7 | | equequ2 2025 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → (𝑡 = 𝑏 ↔ 𝑡 = 𝑎)) |
| 8 | | neeq1 3003 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → (𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐)) |
| 9 | 7, 8 | 3anbi13d 1440 |
. . . . . 6
⊢ (𝑏 = 𝑎 → ((𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))) |
| 10 | 9 | exbidv 1921 |
. . . . 5
⊢ (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))) |
| 11 | 10 | cbvexvw 2036 |
. . . 4
⊢
(∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)) |
| 12 | 11 | exbii 1848 |
. . 3
⊢
(∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)) |
| 13 | 12 | a1i 11 |
. 2
⊢ (𝑏 = 𝑎 → (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))) |
| 14 | | equequ1 2024 |
. . . . . . 7
⊢ (𝑡 = 𝑏 → (𝑡 = 𝑎 ↔ 𝑏 = 𝑎)) |
| 15 | | neeq1 3003 |
. . . . . . 7
⊢ (𝑡 = 𝑏 → (𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐)) |
| 16 | 14, 15 | 3anbi12d 1439 |
. . . . . 6
⊢ (𝑡 = 𝑏 → ((𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))) |
| 17 | 16 | 2exbidv 1924 |
. . . . 5
⊢ (𝑡 = 𝑏 → (∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))) |
| 18 | 17 | cbvexvw 2036 |
. . . 4
⊢
(∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)) |
| 19 | | excom 2162 |
. . . . 5
⊢
(∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)) |
| 20 | | 3ancomb 1099 |
. . . . . . 7
⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 21 | | equcom 2017 |
. . . . . . . 8
⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏) |
| 22 | 21 | 3anbi1i 1158 |
. . . . . . 7
⊢ ((𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 23 | 20, 22 | bitri 275 |
. . . . . 6
⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 24 | 23 | 3exbii 1850 |
. . . . 5
⊢
(∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 25 | 19, 24 | bitri 275 |
. . . 4
⊢
(∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 26 | 18, 25 | bitri 275 |
. . 3
⊢
(∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
| 27 | 26 | a1i 11 |
. 2
⊢ (𝑡 = 𝑏 → (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
| 28 | 6, 13, 27 | ichcircshi 47441 |
1
⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) |