Proof of Theorem xoranor
Step | Hyp | Ref
| Expression |
1 | | df-xor 1267 |
. . 3
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
2 | | ax-ia3 101 |
. . . . . . 7
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
3 | 2 | con3d 561 |
. . . . . 6
⊢ (𝜑 → (¬ (𝜑 ∧ 𝜓) → ¬ 𝜓)) |
4 | | olc 632 |
. . . . . 6
⊢ (¬
𝜓 → (¬ 𝜑 ∨ ¬ 𝜓)) |
5 | 3, 4 | syl6 29 |
. . . . 5
⊢ (𝜑 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))) |
6 | | pm3.21 251 |
. . . . . . 7
⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) |
7 | 6 | con3d 561 |
. . . . . 6
⊢ (𝜓 → (¬ (𝜑 ∧ 𝜓) → ¬ 𝜑)) |
8 | | orc 633 |
. . . . . 6
⊢ (¬
𝜑 → (¬ 𝜑 ∨ ¬ 𝜓)) |
9 | 7, 8 | syl6 29 |
. . . . 5
⊢ (𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))) |
10 | 5, 9 | jaoi 636 |
. . . 4
⊢ ((𝜑 ∨ 𝜓) → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))) |
11 | 10 | imdistani 419 |
. . 3
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) → ((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ ¬ 𝜓))) |
12 | 1, 11 | sylbi 114 |
. 2
⊢ ((𝜑 ⊻ 𝜓) → ((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ ¬ 𝜓))) |
13 | | pm3.14 670 |
. . . 4
⊢ ((¬
𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
14 | 13 | anim2i 324 |
. . 3
⊢ (((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ ¬ 𝜓)) → ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
15 | 14, 1 | sylibr 137 |
. 2
⊢ (((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ ¬ 𝜓)) → (𝜑 ⊻ 𝜓)) |
16 | 12, 15 | impbii 117 |
1
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ ¬ 𝜓))) |