ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfandc GIF version

Theorem dfandc 822
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.)
Assertion
Ref Expression
dfandc (DECID 𝜑 → (DECID 𝜓 → ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))))

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 606 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 123 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
3 simplimdc 801 . . . . . . 7 (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
43adantr 272 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
54imp 123 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑)
6 simprimdc 800 . . . . . . 7 (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
76adantl 273 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
87imp 123 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓)
95, 8jca 302 . . . 4 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → (𝜑𝜓))
109ex 114 . . 3 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → (𝜑𝜓)))
112, 10impbid2 142 . 2 ((DECID 𝜑DECID 𝜓) → ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))
1211ex 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