Proof of Theorem nebidc
Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) |
2 | 1 | necon3bid 2246 |
. . 3
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
3 | | id 19 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
4 | 3 | a1d 22 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))) |
5 | 4 | a1d 22 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) |
6 | 5 | necon4biddc 2280 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))) |
7 | 6 | com3l 75 |
. . . 4
⊢
(DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))) |
8 | 7 | imp 115 |
. . 3
⊢
((DECID 𝐴 = 𝐵 ∧ DECID 𝐶 = 𝐷) → ((𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))) |
9 | 2, 8 | impbid2 131 |
. 2
⊢
((DECID 𝐴 = 𝐵 ∧ DECID 𝐶 = 𝐷) → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))) |
10 | 9 | ex 108 |
1
⊢
(DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) |