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  6970  nn0n0n1ge2b  9305  gcdmndc  11912  gcdsupex  11925  gcdsupcl  11926  gcdaddm  11952  nnwosdc  12007  lcmval  12030  lcmcllem  12034  lcmledvds  12037  prmdc  12097  pclemdc  12255  pcmptdvds  12310  infpnlem2  12325  1arith  12332  ctiunctlemudc  12405  nninfdclemcl  12416  nninfdclemp1  12418  lgsval  13976  lgscllem  13979  lgsneg  13996  lgsdir  14007  lgsdi  14009  lgsne0  14010  nninfsellemdc  14320