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

Proof of Theorem dcan2

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

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  6958  nn0n0n1ge2b  9291  gcdmndc  11899  gcdsupex  11912  gcdsupcl  11913  gcdaddm  11939  nnwosdc  11994  lcmval  12017  lcmcllem  12021  lcmledvds  12024  prmdc  12084  pclemdc  12242  pcmptdvds  12297  infpnlem2  12312  1arith  12319  ctiunctlemudc  12392  nninfdclemcl  12403  nninfdclemp1  12405  lgsval  13699  lgscllem  13702  lgsneg  13719  lgsdir  13730  lgsdi  13732  lgsne0  13733  nninfsellemdc  14043