Proof of Theorem dcan
Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . . 6
⊢ ((¬
φ ∧
ψ) → ¬ φ) |
2 | 1 | intnanrd 840 |
. . . . 5
⊢ ((¬
φ ∧
ψ) → ¬ (φ ∧ ψ)) |
3 | 2 | orim2i 677 |
. . . 4
⊢ (((φ ∧ ψ) ∨ (¬
φ ∧
ψ)) → ((φ ∧ ψ) ∨ ¬
(φ ∧
ψ))) |
4 | | simpr 103 |
. . . . . 6
⊢ (((φ ∨ ¬
φ) ∧
¬ ψ) → ¬ ψ) |
5 | 4 | intnand 839 |
. . . . 5
⊢ (((φ ∨ ¬
φ) ∧
¬ ψ) → ¬ (φ ∧ ψ)) |
6 | 5 | olcd 652 |
. . . 4
⊢ (((φ ∨ ¬
φ) ∧
¬ ψ) → ((φ ∧ ψ) ∨ ¬
(φ ∧
ψ))) |
7 | 3, 6 | jaoi 635 |
. . 3
⊢ ((((φ ∧ ψ) ∨ (¬
φ ∧
ψ)) ∨
((φ ∨
¬ φ) ∧ ¬ ψ))
→ ((φ ∧ ψ) ∨ ¬ (φ
∧ ψ))) |
8 | | df-dc 742 |
. . . . 5
⊢
(DECID φ ↔
(φ ∨
¬ φ)) |
9 | | df-dc 742 |
. . . . 5
⊢
(DECID ψ ↔
(ψ ∨
¬ ψ)) |
10 | 8, 9 | anbi12i 433 |
. . . 4
⊢
((DECID φ ∧ DECID ψ) ↔ ((φ ∨ ¬
φ) ∧
(ψ ∨
¬ ψ))) |
11 | | andi 730 |
. . . 4
⊢ (((φ ∨ ¬
φ) ∧
(ψ ∨
¬ ψ)) ↔ (((φ ∨ ¬
φ) ∧
ψ) ∨
((φ ∨
¬ φ) ∧ ¬ ψ))) |
12 | | andir 731 |
. . . . 5
⊢ (((φ ∨ ¬
φ) ∧
ψ) ↔ ((φ ∧ ψ) ∨ (¬
φ ∧
ψ))) |
13 | 12 | orbi1i 679 |
. . . 4
⊢ ((((φ ∨ ¬
φ) ∧
ψ) ∨
((φ ∨
¬ φ) ∧ ¬ ψ))
↔ (((φ ∧ ψ) ∨ (¬ φ
∧ ψ))
∨ ((φ
∨ ¬ φ) ∧ ¬
ψ))) |
14 | 10, 11, 13 | 3bitri 195 |
. . 3
⊢
((DECID φ ∧ DECID ψ) ↔ (((φ ∧ ψ) ∨ (¬
φ ∧
ψ)) ∨
((φ ∨
¬ φ) ∧ ¬ ψ))) |
15 | | df-dc 742 |
. . 3
⊢
(DECID (φ ∧ ψ) ↔
((φ ∧
ψ) ∨
¬ (φ ∧ ψ))) |
16 | 7, 14, 15 | 3imtr4i 190 |
. 2
⊢
((DECID φ ∧ DECID ψ) → DECID (φ ∧ ψ)) |
17 | 16 | ex 108 |
1
⊢
(DECID φ →
(DECID ψ →
DECID (φ ∧ ψ))) |