Proof of Theorem or3or
Step | Hyp | Ref
| Expression |
1 | | excxor 1500 |
. . 3
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) |
2 | 1 | orbi2i 906 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))) |
3 | | orc 861 |
. . . 4
⊢ (𝜑 → (𝜑 ∨ 𝜓)) |
4 | | exmid 888 |
. . . . 5
⊢ (𝜓 ∨ ¬ 𝜓) |
5 | | pm3.2 470 |
. . . . . 6
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
6 | | biimp 216 |
. . . . . . . . . 10
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
7 | | iman 402 |
. . . . . . . . . 10
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
8 | 6, 7 | sylib 219 |
. . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓)) |
9 | 8 | con2i 141 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ↔ 𝜓)) |
10 | 9 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 ↔ 𝜓))) |
11 | | df-xor 1496 |
. . . . . . . 8
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
12 | 11 | bicomi 225 |
. . . . . . 7
⊢ (¬
(𝜑 ↔ 𝜓) ↔ (𝜑 ⊻ 𝜓)) |
13 | 10, 12 | syl6ib 252 |
. . . . . 6
⊢ (𝜑 → (¬ 𝜓 → (𝜑 ⊻ 𝜓))) |
14 | 5, 13 | orim12d 958 |
. . . . 5
⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
15 | 4, 14 | mpi 20 |
. . . 4
⊢ (𝜑 → ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓))) |
16 | 3, 15 | 2thd 266 |
. . 3
⊢ (𝜑 → ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
17 | | bicom 223 |
. . . . . . 7
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
18 | | bibif 373 |
. . . . . . 7
⊢ (¬
𝜑 → ((𝜓 ↔ 𝜑) ↔ ¬ 𝜓)) |
19 | 17, 18 | syl5bb 284 |
. . . . . 6
⊢ (¬
𝜑 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜓)) |
20 | 19 | con2bid 356 |
. . . . 5
⊢ (¬
𝜑 → (𝜓 ↔ ¬ (𝜑 ↔ 𝜓))) |
21 | 20, 12 | syl6bb 288 |
. . . 4
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ⊻ 𝜓))) |
22 | | biorf 930 |
. . . 4
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
23 | | simpl 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
24 | 23 | con3i 157 |
. . . . 5
⊢ (¬
𝜑 → ¬ (𝜑 ∧ 𝜓)) |
25 | | biorf 930 |
. . . . 5
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (¬
𝜑 → ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
27 | 21, 22, 26 | 3bitr3d 310 |
. . 3
⊢ (¬
𝜑 → ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
28 | 16, 27 | pm2.61i 183 |
. 2
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓))) |
29 | | 3orass 1082 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))) |
30 | 2, 28, 29 | 3bitr4i 304 |
1
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) |