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

Theorem dcan 919
 Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
Assertion
Ref Expression
dcan DECID DECID DECID

Proof of Theorem dcan
StepHypRef Expression
1 simpl 108 . . . . . 6
21intnanrd 918 . . . . 5
32orim2i 751 . . . 4
4 simpr 109 . . . . . 6
54intnand 917 . . . . 5
65olcd 724 . . . 4
73, 6jaoi 706 . . 3
8 df-dc 821 . . . . 5 DECID
9 df-dc 821 . . . . 5 DECID
108, 9anbi12i 456 . . . 4 DECID DECID
11 andi 808 . . . 4
12 andir 809 . . . . 5
1312orbi1i 753 . . . 4
1410, 11, 133bitri 205 . . 3 DECID DECID
15 df-dc 821 . . 3 DECID
167, 14, 153imtr4i 200 . 2 DECID DECID DECID
1716ex 114 1 DECID DECID DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 698  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-dc 821 This theorem is referenced by:  dcbi  921  annimdc  922  pm4.55dc  923  orandc  924  anordc  941  xordidc  1378  nn0n0n1ge2b  9222  gcdmndc  11804  gcdsupex  11813  gcdsupcl  11814  gcdaddm  11839  lcmval  11911  lcmcllem  11915  lcmledvds  11918  ctiunctlemudc  12117  nninfsellemdc  13523
 Copyright terms: Public domain W3C validator