Proof of Theorem annimdc
Step | Hyp | Ref
| Expression |
1 | | imandc 786 |
. . . 4
⊢
(DECID 𝜓 → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))) |
2 | 1 | adantl 262 |
. . 3
⊢
((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))) |
3 | | dcim 784 |
. . . . 5
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 → 𝜓))) |
4 | 3 | imp 115 |
. . . 4
⊢
((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 → 𝜓)) |
5 | | dcn 746 |
. . . . . 6
⊢
(DECID 𝜓 → DECID ¬ 𝜓) |
6 | | dcan 842 |
. . . . . 6
⊢
(DECID 𝜑 → (DECID ¬ 𝜓 → DECID
(𝜑 ∧ ¬ 𝜓))) |
7 | 5, 6 | syl5 28 |
. . . . 5
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∧ ¬ 𝜓))) |
8 | 7 | imp 115 |
. . . 4
⊢
((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ ¬ 𝜓)) |
9 | | con2bidc 769 |
. . . 4
⊢
(DECID (𝜑 → 𝜓) → (DECID (𝜑 ∧ ¬ 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))) |
10 | 4, 8, 9 | sylc 56 |
. . 3
⊢
((DECID 𝜑 ∧ DECID 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))) |
11 | 2, 10 | mpbid 135 |
. 2
⊢
((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))) |
12 | 11 | ex 108 |
1
⊢
(DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))) |