Proof of Theorem dn1dc
Step | Hyp | Ref
| Expression |
1 | | pm2.45 657 |
. . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) → ¬ 𝜑) |
2 | | imnan 624 |
. . . . 5
⊢ ((¬
(𝜑 ∨ 𝜓) → ¬ 𝜑) ↔ ¬ (¬ (𝜑 ∨ 𝜓) ∧ 𝜑)) |
3 | 1, 2 | mpbi 133 |
. . . 4
⊢ ¬
(¬ (𝜑 ∨ 𝜓) ∧ 𝜑) |
4 | 3 | biorfi 665 |
. . 3
⊢ (𝜒 ↔ (𝜒 ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝜑))) |
5 | | orcom 647 |
. . 3
⊢ ((𝜒 ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝜑)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝜑) ∨ 𝜒)) |
6 | | ordir 730 |
. . 3
⊢ (((¬
(𝜑 ∨ 𝜓) ∧ 𝜑) ∨ 𝜒) ↔ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ 𝜒))) |
7 | 4, 5, 6 | 3bitri 195 |
. 2
⊢ (𝜒 ↔ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ 𝜒))) |
8 | | pm4.45 698 |
. . . . . 6
⊢ (𝜒 ↔ (𝜒 ∧ (𝜒 ∨ 𝜃))) |
9 | | simprrl 491 |
. . . . . . 7
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID 𝜒) |
10 | | dcor 843 |
. . . . . . . . 9
⊢
(DECID 𝜒 → (DECID 𝜃 → DECID
(𝜒 ∨ 𝜃))) |
11 | 10 | imp 115 |
. . . . . . . 8
⊢
((DECID 𝜒 ∧ DECID 𝜃) → DECID (𝜒 ∨ 𝜃)) |
12 | 11 | ad2antll 460 |
. . . . . . 7
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID (𝜒 ∨ 𝜃)) |
13 | | anordc 863 |
. . . . . . 7
⊢
(DECID 𝜒 → (DECID (𝜒 ∨ 𝜃) → ((𝜒 ∧ (𝜒 ∨ 𝜃)) ↔ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))))) |
14 | 9, 12, 13 | sylc 56 |
. . . . . 6
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → ((𝜒 ∧ (𝜒 ∨ 𝜃)) ↔ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) |
15 | 8, 14 | syl5bb 181 |
. . . . 5
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (𝜒 ↔ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) |
16 | 15 | orbi2d 704 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))))) |
17 | 16 | anbi2d 437 |
. . 3
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ 𝜒)) ↔ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))))) |
18 | | dcor 843 |
. . . . . . . 8
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∨ 𝜓))) |
19 | | dcn 746 |
. . . . . . . 8
⊢
(DECID (𝜑 ∨ 𝜓) → DECID ¬ (𝜑 ∨ 𝜓)) |
20 | 18, 19 | syl6 29 |
. . . . . . 7
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID ¬
(𝜑 ∨ 𝜓))) |
21 | 20 | imp 115 |
. . . . . 6
⊢
((DECID 𝜑 ∧ DECID 𝜓) → DECID ¬ (𝜑 ∨ 𝜓)) |
22 | 21 | adantrr 448 |
. . . . 5
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID ¬ (𝜑 ∨ 𝜓)) |
23 | | dcor 843 |
. . . . 5
⊢
(DECID ¬ (𝜑 ∨ 𝜓) → (DECID 𝜒 → DECID
(¬ (𝜑 ∨ 𝜓) ∨ 𝜒))) |
24 | 22, 9, 23 | sylc 56 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID (¬
(𝜑 ∨ 𝜓) ∨ 𝜒)) |
25 | | dcn 746 |
. . . . . . . 8
⊢
(DECID 𝜒 → DECID ¬ 𝜒) |
26 | 9, 25 | syl 14 |
. . . . . . 7
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID ¬ 𝜒) |
27 | | dcn 746 |
. . . . . . . 8
⊢
(DECID (𝜒 ∨ 𝜃) → DECID ¬ (𝜒 ∨ 𝜃)) |
28 | 12, 27 | syl 14 |
. . . . . . 7
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID ¬ (𝜒 ∨ 𝜃)) |
29 | | dcor 843 |
. . . . . . 7
⊢
(DECID ¬ 𝜒 → (DECID ¬ (𝜒 ∨ 𝜃) → DECID (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) |
30 | 26, 28, 29 | sylc 56 |
. . . . . 6
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))) |
31 | | dcn 746 |
. . . . . 6
⊢
(DECID (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)) → DECID ¬ (¬
𝜒 ∨ ¬ (𝜒 ∨ 𝜃))) |
32 | 30, 31 | syl 14 |
. . . . 5
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID ¬ (¬
𝜒 ∨ ¬ (𝜒 ∨ 𝜃))) |
33 | | dcor 843 |
. . . . . 6
⊢
(DECID 𝜑 → (DECID ¬ (¬
𝜒 ∨ ¬ (𝜒 ∨ 𝜃)) → DECID (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))))) |
34 | 33 | imp 115 |
. . . . 5
⊢
((DECID 𝜑 ∧ DECID ¬ (¬
𝜒 ∨ ¬ (𝜒 ∨ 𝜃))) → DECID (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) |
35 | 32, 34 | syldan 266 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → DECID (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) |
36 | | anordc 863 |
. . . 4
⊢
(DECID (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) → (DECID (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))) → (((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ ¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃))))))) |
37 | 24, 35, 36 | sylc 56 |
. . 3
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ ¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))))) |
38 | 17, 37 | bitrd 177 |
. 2
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (((¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∧ (𝜑 ∨ 𝜒)) ↔ ¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))))) |
39 | 7, 38 | syl5rbb 182 |
1
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ 𝜒)) |