![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfandc | GIF version |
Description: Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 606. (Contributed by Jim Kingdon, 30-Apr-2018.) |
Ref | Expression |
---|---|
dfandc | ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2im 606 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 123 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | simplimdc 801 | . . . . . . 7 ⊢ (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑)) | |
4 | 3 | adantr 272 | . . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑)) |
5 | 4 | imp 123 | . . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑) |
6 | simprimdc 800 | . . . . . . 7 ⊢ (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓)) | |
7 | 6 | adantl 273 | . . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓)) |
8 | 7 | imp 123 | . . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓) |
9 | 5, 8 | jca 302 | . . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → (𝜑 ∧ 𝜓)) |
10 | 9 | ex 114 | . . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → (𝜑 ∧ 𝜓))) |
11 | 2, 10 | impbid2 142 | . 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))) |
12 | 11 | ex 114 | 1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 DECID wdc 786 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 |
This theorem depends on definitions: df-bi 116 df-dc 787 |
This theorem is referenced by: pm4.63dc 824 pm4.54dc 849 |
Copyright terms: Public domain | W3C validator |