Proof of Theorem wl-df4-3mintru2
Step | Hyp | Ref
| Expression |
1 | | 3orass 1088 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
2 | | wl-df2-3mintru2 35167 |
. 2
⊢
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
3 | | xor2 1510 |
. . . . . . 7
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
4 | 3 | biancomi 467 |
. . . . . 6
⊢ ((𝜑 ⊻ 𝜓) ↔ (¬ (𝜑 ∧ 𝜓) ∧ (𝜑 ∨ 𝜓))) |
5 | 4 | anbi1ci 629 |
. . . . 5
⊢ ((𝜒 ∧ (𝜑 ⊻ 𝜓)) ↔ ((¬ (𝜑 ∧ 𝜓) ∧ (𝜑 ∨ 𝜓)) ∧ 𝜒)) |
6 | | anass 473 |
. . . . 5
⊢ (((¬
(𝜑 ∧ 𝜓) ∧ (𝜑 ∨ 𝜓)) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∧ ((𝜑 ∨ 𝜓) ∧ 𝜒))) |
7 | 5, 6 | bitri 278 |
. . . 4
⊢ ((𝜒 ∧ (𝜑 ⊻ 𝜓)) ↔ (¬ (𝜑 ∧ 𝜓) ∧ ((𝜑 ∨ 𝜓) ∧ 𝜒))) |
8 | 7 | orbi2i 911 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ (𝜑 ∧ 𝜓) ∧ ((𝜑 ∨ 𝜓) ∧ 𝜒)))) |
9 | | pm5.63 1018 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ ((𝜑 ∨ 𝜓) ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ (𝜑 ∧ 𝜓) ∧ ((𝜑 ∨ 𝜓) ∧ 𝜒)))) |
10 | | andir 1007 |
. . . 4
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
11 | 10 | orbi2i 911 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ ((𝜑 ∨ 𝜓) ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
12 | 8, 9, 11 | 3bitr2i 303 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))) |
13 | 1, 2, 12 | 3bitr4i 307 |
1
⊢
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))) |