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

Theorem dcan2 934
Description: A conjunction of two decidable propositions is decidable, expressed in a curried form as compared to dcan 933. (Contributed by Jim Kingdon, 12-Apr-2018.)
Assertion
Ref Expression
dcan2  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  ( ph  /\  ps )
) )

Proof of Theorem dcan2
StepHypRef Expression
1 dcan 933 . 2  |-  ( (DECID  ph  /\ DECID  ps )  -> DECID 
( ph  /\  ps )
)
21ex 115 1  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  ( ph  /\  ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104  DECID wdc 834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117  df-dc 835
This theorem is referenced by:  dcbi  936  annimdc  937  pm4.55dc  938  orandc  939  anordc  956  xordidc  1399  dcfi  6979  nn0n0n1ge2b  9331  gcdmndc  11944  gcdsupex  11957  gcdsupcl  11958  gcdaddm  11984  nnwosdc  12039  lcmval  12062  lcmcllem  12066  lcmledvds  12069  prmdc  12129  pclemdc  12287  pcmptdvds  12342  infpnlem2  12357  1arith  12364  ctiunctlemudc  12437  nninfdclemcl  12448  nninfdclemp1  12450  lgsval  14375  lgscllem  14378  lgsneg  14395  lgsdir  14406  lgsdi  14408  lgsne0  14409  nninfsellemdc  14729
  Copyright terms: Public domain W3C validator