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

Theorem dfandc 777
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 565. (Contributed by Jim Kingdon, 30-Apr-2018.)
Assertion
Ref Expression
dfandc (DECID φ → (DECID ψ → ((φ ψ) ↔ ¬ (φ → ¬ ψ))))

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 565 . . . 4 (φ → (ψ → ¬ (φ → ¬ ψ)))
21imp 115 . . 3 ((φ ψ) → ¬ (φ → ¬ ψ))
3 simplimdc 756 . . . . . . 7 (DECID φ → (¬ (φ → ¬ ψ) → φ))
43adantr 261 . . . . . 6 ((DECID φ DECID ψ) → (¬ (φ → ¬ ψ) → φ))
54imp 115 . . . . 5 (((DECID φ DECID ψ) ¬ (φ → ¬ ψ)) → φ)
6 simprimdc 755 . . . . . . 7 (DECID ψ → (¬ (φ → ¬ ψ) → ψ))
76adantl 262 . . . . . 6 ((DECID φ DECID ψ) → (¬ (φ → ¬ ψ) → ψ))
87imp 115 . . . . 5 (((DECID φ DECID ψ) ¬ (φ → ¬ ψ)) → ψ)
95, 8jca 290 . . . 4 (((DECID φ DECID ψ) ¬ (φ → ¬ ψ)) → (φ ψ))
109ex 108 . . 3 ((DECID φ DECID ψ) → (¬ (φ → ¬ ψ) → (φ ψ)))
112, 10impbid2 131 . 2 ((DECID φ DECID ψ) → ((φ ψ) ↔ ¬ (φ → ¬ ψ)))
1211ex 108 1 (DECID φ → (DECID ψ → ((φ ψ) ↔ ¬ (φ → ¬ ψ))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98  DECID wdc 741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629
This theorem depends on definitions:  df-bi 110  df-dc 742
This theorem is referenced by:  pm4.63dc  779  pm4.54dc  804
  Copyright terms: Public domain W3C validator