Proof of Theorem dfbi3dc
Step | Hyp | Ref
| Expression |
1 | | dcn 832 |
. . . 4
⊢
(DECID 𝜓 → DECID ¬ 𝜓) |
2 | | xordc 1381 |
. . . . 5
⊢
(DECID 𝜑 → (DECID ¬ 𝜓 → (¬ (𝜑 ↔ ¬ 𝜓) ↔ ((𝜑 ∧ ¬ ¬ 𝜓) ∨ (¬ 𝜓 ∧ ¬ 𝜑))))) |
3 | 2 | imp 123 |
. . . 4
⊢
((DECID 𝜑 ∧ DECID ¬ 𝜓) → (¬ (𝜑 ↔ ¬ 𝜓) ↔ ((𝜑 ∧ ¬ ¬ 𝜓) ∨ (¬ 𝜓 ∧ ¬ 𝜑)))) |
4 | 1, 3 | sylan2 284 |
. . 3
⊢
((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 ↔ ¬ 𝜓) ↔ ((𝜑 ∧ ¬ ¬ 𝜓) ∨ (¬ 𝜓 ∧ ¬ 𝜑)))) |
5 | | pm5.18dc 873 |
. . . 4
⊢
(DECID 𝜑 → (DECID 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)))) |
6 | 5 | imp 123 |
. . 3
⊢
((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓))) |
7 | | notnotbdc 862 |
. . . . . 6
⊢
(DECID 𝜓 → (𝜓 ↔ ¬ ¬ 𝜓)) |
8 | 7 | anbi2d 460 |
. . . . 5
⊢
(DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ¬ ¬ 𝜓))) |
9 | | ancom 264 |
. . . . . 6
⊢ ((¬
𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜓 ∧ ¬ 𝜑)) |
10 | 9 | a1i 9 |
. . . . 5
⊢
(DECID 𝜓 → ((¬ 𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜓 ∧ ¬ 𝜑))) |
11 | 8, 10 | orbi12d 783 |
. . . 4
⊢
(DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ ¬ 𝜓) ∨ (¬ 𝜓 ∧ ¬ 𝜑)))) |
12 | 11 | adantl 275 |
. . 3
⊢
((DECID 𝜑 ∧ DECID 𝜓) → (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ ¬ 𝜓) ∨ (¬ 𝜓 ∧ ¬ 𝜑)))) |
13 | 4, 6, 12 | 3bitr4d 219 |
. 2
⊢
((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)))) |
14 | 13 | ex 114 |
1
⊢
(DECID 𝜑 → (DECID 𝜓 → ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓))))) |