Theorem ancomsd 465

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

Hypothesis

Ref	Expression
ancomsd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
ancomsd	⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Proof of Theorem ancomsd

Step	Hyp	Ref	Expression
1		ancomsd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expcomd 416	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  sylan2d  604  anabsi6  666  mpand  691  2eu3  2656  ralcom2  3290  somo  5539  wereu2  5585  smoel  8175  cfub  9989  cofsmo  10009  grudomon  10557  axpre-sup  10909  leltadd  11442  lemul12b  11815  lbzbi  12658  injresinj  13489  swrdnnn0nd  14350  abslt  15007  absle  15008  o1lo1  15227  o1co  15276  rlimno1  15346  dvdssub2  15991  lublecllem  18059  f1omvdco2  19037  ptpjpre1  22703  iocopnst  24084  ovolicc2lem4  24665  itg2le  24885  ulmcau  25535  cxpeq0  25814  pntrsumbnd2  26696  cvcon3  30625  atexch  30722  abfmpeld  30970  wsuclem  33798  btwntriv2  34293  btwnexch3  34301  isbasisrelowllem1  35505  isbasisrelowllem2  35506  relowlssretop  35513  finxpsuclem  35547  isinf2  35555  finixpnum  35741  fin2solem  35742  ltflcei  35744  poimirlem27  35783  itg2addnclem  35807  unirep  35850  prter2  36874  cvrcon3b  37270  sn-negex12  40378  fltaccoprm  40457  incssnn0  40513  eldioph4b  40613  fphpdo  40619  pellexlem5  40635  pm14.24  42003  icceuelpart  44840  prsprel  44891  sprsymrelfolem2  44897  goldbachthlem2  44950  gbegt5  45165  aacllem  46457