Proof of Theorem cador
Step | Hyp | Ref
| Expression |
1 | | xor2 1513 |
. . . . . . 7
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
2 | 1 | rbaib 539 |
. . . . . 6
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜑 ⊻ 𝜓) ↔ (𝜑 ∨ 𝜓))) |
3 | 2 | anbi1d 630 |
. . . . 5
⊢ (¬
(𝜑 ∧ 𝜓) → (((𝜑 ⊻ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))) |
4 | | ancom 461 |
. . . . 5
⊢ (((𝜑 ⊻ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ⊻ 𝜓))) |
5 | | andir 1006 |
. . . . 5
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
6 | 3, 4, 5 | 3bitr3g 313 |
. . . 4
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜒 ∧ (𝜑 ⊻ 𝜓)) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
7 | 6 | pm5.74i 270 |
. . 3
⊢ ((¬
(𝜑 ∧ 𝜓) → (𝜒 ∧ (𝜑 ⊻ 𝜓))) ↔ (¬ (𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
8 | | df-or 845 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))) ↔ (¬ (𝜑 ∧ 𝜓) → (𝜒 ∧ (𝜑 ⊻ 𝜓)))) |
9 | | df-or 845 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) ↔ (¬ (𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
10 | 7, 8, 9 | 3bitr4i 303 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
11 | | df-cad 1613 |
. 2
⊢
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))) |
12 | | 3orass 1089 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
13 | 10, 11, 12 | 3bitr4i 303 |
1
⊢
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |