Theorem ancomsd 467

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 418	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 412	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  sylan2d  606  anabsi6  669  mpand  694  2eu3  2650  ralcom2  3374  somo  5626  wereu2  5674  smoel  8360  cfub  10244  cofsmo  10264  grudomon  10812  axpre-sup  11164  leltadd  11698  lemul12b  12071  lbzbi  12920  injresinj  13753  swrdnnn0nd  14606  abslt  15261  absle  15262  o1lo1  15481  o1co  15530  rlimno1  15600  dvdssub2  16244  lublecllem  18313  f1omvdco2  19316  ptpjpre1  23075  iocopnst  24456  ovolicc2lem4  25037  itg2le  25257  ulmcau  25907  cxpeq0  26186  pntrsumbnd2  27070  cvcon3  31537  atexch  31634  abfmpeld  31879  wsuclem  34797  btwntriv2  34984  btwnexch3  34992  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlssretop  36244  finxpsuclem  36278  isinf2  36286  finixpnum  36473  fin2solem  36474  ltflcei  36476  poimirlem27  36515  itg2addnclem  36539  unirep  36582  prter2  37751  cvrcon3b  38147  sn-negex12  41289  fltaccoprm  41382  incssnn0  41449  eldioph4b  41549  fphpdo  41555  pellexlem5  41571  pm14.24  43191  icceuelpart  46104  prsprel  46155  sprsymrelfolem2  46161  goldbachthlem2  46214  gbegt5  46429  aacllem  47848