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

Theorem dfandc 870
 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 627. (Contributed by Jim Kingdon, 30-Apr-2018.)
Assertion
Ref Expression
dfandc (DECID 𝜑 → (DECID 𝜓 → ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))))

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 627 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 123 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
3 simplimdc 846 . . . . . . 7 (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
43adantr 274 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
54imp 123 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑)
6 simprimdc 845 . . . . . . 7 (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
76adantl 275 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
87imp 123 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓)
95, 8jca 304 . . . 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 820 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 604  ax-in2 605  ax-io 699 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821 This theorem is referenced by:  pm4.63dc  872  pm4.54dc  888
 Copyright terms: Public domain W3C validator