Proof of Theorem dn1dc
Step | Hyp | Ref
| Expression |
1 | | pm2.45 656 |
. . . . 5
⊢ (¬
(φ ∨
ψ) → ¬ φ) |
2 | | imnan 623 |
. . . . 5
⊢ ((¬
(φ ∨
ψ) → ¬ φ) ↔ ¬ (¬ (φ ∨ ψ) ∧ φ)) |
3 | 1, 2 | mpbi 133 |
. . . 4
⊢ ¬
(¬ (φ
∨ ψ) ∧ φ) |
4 | 3 | biorfi 664 |
. . 3
⊢ (χ ↔ (χ ∨ (¬
(φ ∨
ψ) ∧
φ))) |
5 | | orcom 646 |
. . 3
⊢ ((χ ∨ (¬
(φ ∨
ψ) ∧
φ)) ↔ ((¬ (φ ∨ ψ) ∧ φ) ∨ χ)) |
6 | | ordir 729 |
. . 3
⊢ (((¬
(φ ∨
ψ) ∧
φ) ∨
χ) ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ))) |
7 | 4, 5, 6 | 3bitri 195 |
. 2
⊢ (χ ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ))) |
8 | | pm4.45 697 |
. . . . . 6
⊢ (χ ↔ (χ ∧ (χ ∨ θ))) |
9 | | simprrl 491 |
. . . . . . 7
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID χ) |
10 | | dcor 842 |
. . . . . . . . 9
⊢
(DECID χ →
(DECID θ →
DECID (χ ∨ θ))) |
11 | 10 | imp 115 |
. . . . . . . 8
⊢
((DECID χ ∧ DECID θ) → DECID (χ ∨ θ)) |
12 | 11 | ad2antll 460 |
. . . . . . 7
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID (χ ∨ θ)) |
13 | | anordc 862 |
. . . . . . 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 703 |
. . . 4
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → ((φ ∨ χ) ↔ (φ ∨ ¬
(¬ χ
∨ ¬ (χ ∨ θ))))) |
17 | 16 | anbi2d 437 |
. . 3
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → (((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ)) ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ ¬
(¬ χ
∨ ¬ (χ ∨ θ)))))) |
18 | | dcor 842 |
. . . . . . . 8
⊢
(DECID φ →
(DECID ψ →
DECID (φ ∨ ψ))) |
19 | | dcn 745 |
. . . . . . . 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 842 |
. . . . 5
⊢
(DECID ¬ (φ
∨ ψ)
→ (DECID χ →
DECID (¬ (φ ∨ ψ) ∨ χ))) |
24 | 22, 9, 23 | sylc 56 |
. . . 4
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID (¬
(φ ∨
ψ) ∨
χ)) |
25 | | dcn 745 |
. . . . . . . 8
⊢
(DECID χ →
DECID ¬ χ) |
26 | 9, 25 | syl 14 |
. . . . . . 7
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID ¬
χ) |
27 | | dcn 745 |
. . . . . . . 8
⊢
(DECID (χ ∨ θ)
→ DECID ¬ (χ
∨ θ)) |
28 | 12, 27 | syl 14 |
. . . . . . 7
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID ¬
(χ ∨
θ)) |
29 | | dcor 842 |
. . . . . . 7
⊢
(DECID ¬ χ
→ (DECID ¬ (χ
∨ θ)
→ DECID (¬ χ
∨ ¬ (χ ∨ θ)))) |
30 | 26, 28, 29 | sylc 56 |
. . . . . 6
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID (¬
χ ∨
¬ (χ
∨ θ))) |
31 | | dcn 745 |
. . . . . 6
⊢
(DECID (¬ χ
∨ ¬ (χ ∨ θ)) → DECID ¬
(¬ χ
∨ ¬ (χ ∨ θ))) |
32 | 30, 31 | syl 14 |
. . . . 5
⊢
((DECID φ ∧ (DECID ψ ∧
(DECID χ ∧ DECID θ))) → DECID ¬
(¬ χ
∨ ¬ (χ ∨ θ))) |
33 | | dcor 842 |
. . . . . 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 862 |
. . . 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 θ))) → (¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬
(φ ∨
¬ (¬ χ
∨ ¬ (χ ∨ θ))))
↔ χ)) |