Theorem dcan2 924

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

Assertion

Ref	Expression
dcan2	⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓)))

Proof of Theorem dcan2

Step	Hyp	Ref	Expression
1		dcan 923	. 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ 𝜓))
2	1	ex 114	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 824

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 825

This theorem is referenced by:  dcbi  926  annimdc  927  pm4.55dc  928  orandc  929  anordc  946  xordidc  1389  dcfi  6942  nn0n0n1ge2b  9266  gcdmndc  11873  gcdsupex  11886  gcdsupcl  11887  gcdaddm  11913  nnwosdc  11968  lcmval  11991  lcmcllem  11995  lcmledvds  11998  prmdc  12058  pclemdc  12216  pcmptdvds  12271  infpnlem2  12286  1arith  12293  ctiunctlemudc  12366  nninfdclemcl  12377  nninfdclemp1  12379  lgsval  13505  lgscllem  13508  lgsneg  13525  lgsdir  13536  lgsdi  13538  lgsne0  13539  nninfsellemdc  13850