Proof of Theorem or3or
Step | Hyp | Ref
| Expression |
1 | | excxor 1507 |
. . 3
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) |
2 | 1 | orbi2i 909 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))) |
3 | | orc 863 |
. . . 4
⊢ (𝜑 → (𝜑 ∨ 𝜓)) |
4 | | exmid 891 |
. . . . 5
⊢ (𝜓 ∨ ¬ 𝜓) |
5 | | pm3.2 472 |
. . . . . 6
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
6 | | biimp 217 |
. . . . . . . . . 10
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
7 | | iman 404 |
. . . . . . . . . 10
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
8 | 6, 7 | sylib 220 |
. . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓)) |
9 | 8 | con2i 141 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ↔ 𝜓)) |
10 | 9 | ex 415 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 ↔ 𝜓))) |
11 | | df-xor 1502 |
. . . . . . . 8
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
12 | 11 | bicomi 226 |
. . . . . . 7
⊢ (¬
(𝜑 ↔ 𝜓) ↔ (𝜑 ⊻ 𝜓)) |
13 | 10, 12 | syl6ib 253 |
. . . . . 6
⊢ (𝜑 → (¬ 𝜓 → (𝜑 ⊻ 𝜓))) |
14 | 5, 13 | orim12d 961 |
. . . . 5
⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
15 | 4, 14 | mpi 20 |
. . . 4
⊢ (𝜑 → ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓))) |
16 | 3, 15 | 2thd 267 |
. . 3
⊢ (𝜑 → ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
17 | | bicom 224 |
. . . . . . 7
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
18 | | bibif 374 |
. . . . . . 7
⊢ (¬
𝜑 → ((𝜓 ↔ 𝜑) ↔ ¬ 𝜓)) |
19 | 17, 18 | syl5bb 285 |
. . . . . 6
⊢ (¬
𝜑 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜓)) |
20 | 19 | con2bid 357 |
. . . . 5
⊢ (¬
𝜑 → (𝜓 ↔ ¬ (𝜑 ↔ 𝜓))) |
21 | 20, 12 | syl6bb 289 |
. . . 4
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ⊻ 𝜓))) |
22 | | biorf 933 |
. . . 4
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
23 | | simpl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
24 | 23 | con3i 157 |
. . . . 5
⊢ (¬
𝜑 → ¬ (𝜑 ∧ 𝜓)) |
25 | | biorf 933 |
. . . . 5
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (¬
𝜑 → ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
27 | 21, 22, 26 | 3bitr3d 311 |
. . 3
⊢ (¬
𝜑 → ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓)))) |
28 | 16, 27 | pm2.61i 184 |
. 2
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ⊻ 𝜓))) |
29 | | 3orass 1086 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))) |
30 | 2, 28, 29 | 3bitr4i 305 |
1
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) |