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

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

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 599 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 122 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
3 simplimdc 793 . . . . . . 7 (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
43adantr 270 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
54imp 122 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑)
6 simprimdc 792 . . . . . . 7 (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
76adantl 271 . . . . . 6 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
87imp 122 . . . . 5 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓)
95, 8jca 300 . . . 4 (((DECID 𝜑DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → (𝜑𝜓))
109ex 113 . . 3 ((DECID 𝜑DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → (𝜑𝜓)))
112, 10impbid2 141 . 2 ((DECID 𝜑DECID 𝜓) → ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))
1211ex 113 1 (DECID 𝜑 → (DECID 𝜓 → ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  DECID wdc 778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115  df-dc 779
This theorem is referenced by:  pm4.63dc  816  pm4.54dc  841
  Copyright terms: Public domain W3C validator