Proof of Theorem ifpdfxor
Step | Hyp | Ref
| Expression |
1 | | xor2 1513 |
. 2
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
2 | | ifpdfor 40649 |
. . 3
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) |
3 | | ifpnot23 40662 |
. . . 4
⊢ (¬
if-(𝜑, 𝜓, ⊥) ↔ if-(𝜑, ¬ 𝜓, ¬ ⊥)) |
4 | | ifpdfan 40650 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) |
5 | 3, 4 | xchnxbir 336 |
. . 3
⊢ (¬
(𝜑 ∧ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ¬ ⊥)) |
6 | 2, 5 | anbi12i 630 |
. 2
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (if-(𝜑, ⊤, 𝜓) ∧ if-(𝜑, ¬ 𝜓, ¬ ⊥))) |
7 | | ifpan23 40644 |
. . 3
⊢
((if-(𝜑, ⊤,
𝜓) ∧ if-(𝜑, ¬ 𝜓, ¬ ⊥)) ↔ if-(𝜑, (⊤ ∧ ¬ 𝜓), (𝜓 ∧ ¬ ⊥))) |
8 | | truan 1553 |
. . . 4
⊢
((⊤ ∧ ¬ 𝜓) ↔ ¬ 𝜓) |
9 | | fal 1556 |
. . . . . 6
⊢ ¬
⊥ |
10 | 9 | biantru 533 |
. . . . 5
⊢ (𝜓 ↔ (𝜓 ∧ ¬ ⊥)) |
11 | 10 | bicomi 227 |
. . . 4
⊢ ((𝜓 ∧ ¬ ⊥) ↔ 𝜓) |
12 | | ifpbi23 40657 |
. . . 4
⊢
((((⊤ ∧ ¬ 𝜓) ↔ ¬ 𝜓) ∧ ((𝜓 ∧ ¬ ⊥) ↔ 𝜓)) → (if-(𝜑, (⊤ ∧ ¬ 𝜓), (𝜓 ∧ ¬ ⊥)) ↔ if-(𝜑, ¬ 𝜓, 𝜓))) |
13 | 8, 11, 12 | mp2an 692 |
. . 3
⊢
(if-(𝜑, (⊤
∧ ¬ 𝜓), (𝜓 ∧ ¬ ⊥)) ↔
if-(𝜑, ¬ 𝜓, 𝜓)) |
14 | 7, 13 | bitri 278 |
. 2
⊢
((if-(𝜑, ⊤,
𝜓) ∧ if-(𝜑, ¬ 𝜓, ¬ ⊥)) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) |
15 | 1, 6, 14 | 3bitri 300 |
1
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) |