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

Theorem dfandc 778
 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 566. (Contributed by Jim Kingdon, 30-Apr-2018.)
Assertion
Ref Expression
dfandc DECID DECID

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 566 . . . 4
21imp 115 . . 3
3 simplimdc 757 . . . . . . 7 DECID
43adantr 261 . . . . . 6 DECID DECID
54imp 115 . . . . 5 DECID DECID
6 simprimdc 756 . . . . . . 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 742 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 630 This theorem depends on definitions:  df-bi 110  df-dc 743 This theorem is referenced by:  pm4.63dc  780  pm4.54dc  805
 Copyright terms: Public domain W3C validator