Proof of Theorem dcor
Step | Hyp | Ref
| Expression |
1 | | df-dc 742 |
. 2
⊢
(DECID φ ↔
(φ ∨
¬ φ)) |
2 | | orc 632 |
. . . . . 6
⊢ (φ → (φ ∨ ψ)) |
3 | 2 | orcd 651 |
. . . . 5
⊢ (φ → ((φ ∨ ψ) ∨ ¬
(φ ∨
ψ))) |
4 | | df-dc 742 |
. . . . 5
⊢
(DECID (φ ∨ ψ) ↔
((φ ∨
ψ) ∨
¬ (φ
∨ ψ))) |
5 | 3, 4 | sylibr 137 |
. . . 4
⊢ (φ → DECID (φ ∨ ψ)) |
6 | 5 | a1d 22 |
. . 3
⊢ (φ → (DECID ψ → DECID (φ ∨ ψ))) |
7 | | df-dc 742 |
. . . . 5
⊢
(DECID ψ ↔
(ψ ∨
¬ ψ)) |
8 | | olc 631 |
. . . . . . . . 9
⊢ (ψ → (φ ∨ ψ)) |
9 | 8 | adantl 262 |
. . . . . . . 8
⊢ ((¬
φ ∧
ψ) → (φ ∨ ψ)) |
10 | 9 | orcd 651 |
. . . . . . 7
⊢ ((¬
φ ∧
ψ) → ((φ ∨ ψ) ∨ ¬
(φ ∨
ψ))) |
11 | 10, 4 | sylibr 137 |
. . . . . 6
⊢ ((¬
φ ∧
ψ) → DECID (φ ∨ ψ)) |
12 | | ioran 668 |
. . . . . . . . 9
⊢ (¬
(φ ∨
ψ) ↔ (¬ φ ∧ ¬
ψ)) |
13 | 12 | biimpri 124 |
. . . . . . . 8
⊢ ((¬
φ ∧
¬ ψ) → ¬ (φ ∨ ψ)) |
14 | 13 | olcd 652 |
. . . . . . 7
⊢ ((¬
φ ∧
¬ ψ) → ((φ ∨ ψ) ∨ ¬
(φ ∨
ψ))) |
15 | 14, 4 | sylibr 137 |
. . . . . 6
⊢ ((¬
φ ∧
¬ ψ) → DECID
(φ ∨
ψ)) |
16 | 11, 15 | jaodan 709 |
. . . . 5
⊢ ((¬
φ ∧
(ψ ∨
¬ ψ)) → DECID
(φ ∨
ψ)) |
17 | 7, 16 | sylan2b 271 |
. . . 4
⊢ ((¬
φ ∧
DECID ψ) →
DECID (φ ∨ ψ)) |
18 | 17 | ex 108 |
. . 3
⊢ (¬
φ → (DECID ψ → DECID (φ ∨ ψ))) |
19 | 6, 18 | jaoi 635 |
. 2
⊢ ((φ ∨ ¬
φ) → (DECID ψ → DECID (φ ∨ ψ))) |
20 | 1, 19 | sylbi 114 |
1
⊢
(DECID φ →
(DECID ψ →
DECID (φ ∨ ψ))) |