Proof of Theorem dcim
Step | Hyp | Ref
| Expression |
1 | | df-dc 835 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
2 | | df-dc 835 |
. . . . . . . 8
⊢
(DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓)) |
3 | 2 | anbi2i 457 |
. . . . . . 7
⊢ ((𝜑 ∧ DECID 𝜓) ↔ (𝜑 ∧ (𝜓 ∨ ¬ 𝜓))) |
4 | | andi 818 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) |
5 | 3, 4 | bitri 184 |
. . . . . 6
⊢ ((𝜑 ∧ DECID 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) |
6 | | pm3.4 333 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓)) |
7 | | annimim 686 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 → 𝜓)) |
8 | 6, 7 | orim12i 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
9 | 5, 8 | sylbi 121 |
. . . . 5
⊢ ((𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
10 | | df-dc 835 |
. . . . 5
⊢
(DECID (𝜑 → 𝜓) ↔ ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
11 | 9, 10 | sylibr 134 |
. . . 4
⊢ ((𝜑 ∧ DECID 𝜓) → DECID
(𝜑 → 𝜓)) |
12 | 11 | ex 115 |
. . 3
⊢ (𝜑 → (DECID
𝜓 → DECID
(𝜑 → 𝜓))) |
13 | | ax-in2 615 |
. . . . 5
⊢ (¬
𝜑 → (𝜑 → 𝜓)) |
14 | 13 | a1d 22 |
. . . 4
⊢ (¬
𝜑 →
(DECID 𝜓
→ (𝜑 → 𝜓))) |
15 | | orc 712 |
. . . . 5
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜓) ∨ ¬ (𝜑 → 𝜓))) |
16 | 15, 10 | sylibr 134 |
. . . 4
⊢ ((𝜑 → 𝜓) → DECID (𝜑 → 𝜓)) |
17 | 14, 16 | syl6 33 |
. . 3
⊢ (¬
𝜑 →
(DECID 𝜓
→ DECID (𝜑 → 𝜓))) |
18 | 12, 17 | jaoi 716 |
. 2
⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID
(𝜑 → 𝜓))) |
19 | 1, 18 | sylbi 121 |
1
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 → 𝜓))) |