Theorem dcan2 929

Description: A conjunction of two decidable propositions is decidable, expressed in a curried form as compared to dcan 928. (Contributed by Jim Kingdon, 12-Apr-2018.)

Assertion

Ref	Expression
dcan2	|- (DECID ph -> (DECID ps -> DECID ( ph /\ ps ) ) )

Proof of Theorem dcan2

Step	Hyp	Ref	Expression
1		dcan 928	. 2 |- ( (DECID ph /\ DECID ps ) -> DECID ( ph /\ ps ) )
2	1	ex 114	1 |- (DECID ph -> (DECID ps -> DECID ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 103  DECID wdc 829

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 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116  df-dc 830

This theorem is referenced by:  dcbi  931  annimdc  932  pm4.55dc  933  orandc  934  anordc  951  xordidc  1394  dcfi  6956  nn0n0n1ge2b  9284  gcdmndc  11892  gcdsupex  11905  gcdsupcl  11906  gcdaddm  11932  nnwosdc  11987  lcmval  12010  lcmcllem  12014  lcmledvds  12017  prmdc  12077  pclemdc  12235  pcmptdvds  12290  infpnlem2  12305  1arith  12312  ctiunctlemudc  12385  nninfdclemcl  12396  nninfdclemp1  12398  lgsval  13664  lgscllem  13667  lgsneg  13684  lgsdir  13695  lgsdi  13697  lgsne0  13698  nninfsellemdc  14008