Proof of Theorem xordc1
Step | Hyp | Ref
| Expression |
1 | | andir 732 |
. . 3
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ ((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) ∨ (𝜓 ∧ ¬ (𝜑 ∧ 𝜓)))) |
2 | | simpl 102 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) → 𝜑) |
3 | | imnan 624 |
. . . . . 6
⊢ ((𝜓 → ¬ 𝜑) ↔ ¬ (𝜓 ∧ 𝜑)) |
4 | | ancom 253 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) |
5 | 3, 4 | xchbinxr 608 |
. . . . 5
⊢ ((𝜓 → ¬ 𝜑) ↔ ¬ (𝜑 ∧ 𝜓)) |
6 | | pm3.35 329 |
. . . . 5
⊢ ((𝜓 ∧ (𝜓 → ¬ 𝜑)) → ¬ 𝜑) |
7 | 5, 6 | sylan2br 272 |
. . . 4
⊢ ((𝜓 ∧ ¬ (𝜑 ∧ 𝜓)) → ¬ 𝜑) |
8 | 2, 7 | orim12i 676 |
. . 3
⊢ (((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) ∨ (𝜓 ∧ ¬ (𝜑 ∧ 𝜓))) → (𝜑 ∨ ¬ 𝜑)) |
9 | 1, 8 | sylbi 114 |
. 2
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) → (𝜑 ∨ ¬ 𝜑)) |
10 | | df-xor 1267 |
. 2
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
11 | | df-dc 743 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
12 | 9, 10, 11 | 3imtr4i 190 |
1
⊢ ((𝜑 ⊻ 𝜓) → DECID 𝜑) |