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 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓)))

Proof of Theorem dcan2

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

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  6982  nn0n0n1ge2b  9334  gcdmndc  11947  gcdsupex  11960  gcdsupcl  11961  gcdaddm  11987  nnwosdc  12042  lcmval  12065  lcmcllem  12069  lcmledvds  12072  prmdc  12132  pclemdc  12290  pcmptdvds  12345  infpnlem2  12360  1arith  12367  ctiunctlemudc  12440  nninfdclemcl  12451  nninfdclemp1  12453  lgsval  14490  lgscllem  14493  lgsneg  14510  lgsdir  14521  lgsdi  14523  lgsne0  14524  nninfsellemdc  14844