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 626. (Contributed by Jim Kingdon, 30-Apr-2018.) |
Ref | Expression |
---|---|
dfandc | ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2im 626 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 123 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | simplimdc 845 | . . . . . . 7 ⊢ (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑)) | |
4 | 3 | adantr 274 | . . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑)) |
5 | 4 | imp 123 | . . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑) |
6 | simprimdc 844 | . . . . . . 7 ⊢ (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓)) | |
7 | 6 | adantl 275 | . . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓)) |
8 | 7 | imp 123 | . . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓) |
9 | 5, 8 | jca 304 | . . . 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 819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 |
This theorem depends on definitions: df-bi 116 df-stab 816 df-dc 820 |
This theorem is referenced by: pm4.63dc 871 pm4.54dc 887 |
Copyright terms: Public domain | W3C validator |