Proof of Theorem dcim
Step | Hyp | Ref
| Expression |
1 | | df-dc 830 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
2 | | df-dc 830 |
. . . . . . . 8
⊢
(DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓)) |
3 | 2 | anbi2i 454 |
. . . . . . 7
⊢ ((𝜑 ∧ DECID 𝜓) ↔ (𝜑 ∧ (𝜓 ∨ ¬ 𝜓))) |
4 | | andi 813 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) |
5 | 3, 4 | bitri 183 |
. . . . . 6
⊢ ((𝜑 ∧ DECID 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) |
6 | | pm3.4 331 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓)) |
7 | | annimim 681 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 → 𝜓)) |
8 | 6, 7 | orim12i 754 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
9 | 5, 8 | sylbi 120 |
. . . . 5
⊢ ((𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
10 | | df-dc 830 |
. . . . 5
⊢
(DECID (𝜑 → 𝜓) ↔ ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
11 | 9, 10 | sylibr 133 |
. . . 4
⊢ ((𝜑 ∧ DECID 𝜓) → DECID
(𝜑 → 𝜓)) |
12 | 11 | ex 114 |
. . 3
⊢ (𝜑 → (DECID
𝜓 → DECID
(𝜑 → 𝜓))) |
13 | | ax-in2 610 |
. . . . 5
⊢ (¬
𝜑 → (𝜑 → 𝜓)) |
14 | 13 | a1d 22 |
. . . 4
⊢ (¬
𝜑 →
(DECID 𝜓
→ (𝜑 → 𝜓))) |
15 | | orc 707 |
. . . . 5
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
16 | 15, 10 | sylibr 133 |
. . . 4
⊢ ((𝜑 → 𝜓) → DECID (𝜑 → 𝜓)) |
17 | 14, 16 | syl6 33 |
. . 3
⊢ (¬
𝜑 →
(DECID 𝜓
→ DECID (𝜑 → 𝜓))) |
18 | 12, 17 | jaoi 711 |
. 2
⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID
(𝜑 → 𝜓))) |
19 | 1, 18 | sylbi 120 |
1
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 → 𝜓))) |