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  31568  atexch  31665  abfmpeld  31910  wsuclem  34828  btwntriv2  35015  btwnexch3  35023  isbasisrelowllem1  36284  isbasisrelowllem2  36285  relowlssretop  36292  finxpsuclem  36326  isinf2  36334  finixpnum  36521  fin2solem  36522  ltflcei  36524  poimirlem27  36563  itg2addnclem  36587  unirep  36630  prter2  37799  cvrcon3b  38195  sn-negex12  41337  fltaccoprm  41430  incssnn0  41497  eldioph4b  41597  fphpdo  41603  pellexlem5  41619  pm14.24  43239  icceuelpart  46152  prsprel  46203  sprsymrelfolem2  46209  goldbachthlem2  46262  gbegt5  46477  aacllem  47896