Proof of Theorem elprneb
Step | Hyp | Ref
| Expression |
1 | | elpri 4648 |
. . 3
⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
2 | | neeq1 3004 |
. . . . . 6
⊢ (𝐵 = 𝐴 → (𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶)) |
3 | 2 | eqcoms 2741 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶)) |
4 | | pm5.1 823 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) |
5 | 4 | ex 414 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
6 | 3, 5 | sylbid 239 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝐵 ≠ 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
7 | | neeq2 3005 |
. . . . 5
⊢ (𝐴 = 𝐶 → (𝐵 ≠ 𝐴 ↔ 𝐵 ≠ 𝐶)) |
8 | | nesym 2998 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐵) |
9 | | pm5.1 823 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ ¬ 𝐴 = 𝐵) → (𝐴 = 𝐶 ↔ ¬ 𝐴 = 𝐵)) |
10 | 8, 9 | sylan2b 595 |
. . . . . . 7
⊢ ((𝐴 = 𝐶 ∧ 𝐵 ≠ 𝐴) → (𝐴 = 𝐶 ↔ ¬ 𝐴 = 𝐵)) |
11 | 10 | necon2abid 2984 |
. . . . . 6
⊢ ((𝐴 = 𝐶 ∧ 𝐵 ≠ 𝐴) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) |
12 | 11 | ex 414 |
. . . . 5
⊢ (𝐴 = 𝐶 → (𝐵 ≠ 𝐴 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
13 | 7, 12 | sylbird 260 |
. . . 4
⊢ (𝐴 = 𝐶 → (𝐵 ≠ 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
14 | 6, 13 | jaoi 856 |
. . 3
⊢ ((𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → (𝐵 ≠ 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
15 | 1, 14 | syl 17 |
. 2
⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐵 ≠ 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))) |
16 | 15 | imp 408 |
1
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) |