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 207  df-an 396

This theorem is referenced by:  sylan2d  606  anabsi6  671  mpand  696  2eu3  2655  ralcom2  3340  somo  5578  wereu2  5628  smoel  8300  cfub  10171  cofsmo  10191  grudomon  10740  axpre-sup  11092  leltadd  11634  lemul12b  12012  lbzbi  12886  injresinj  13746  swrdnnn0nd  14619  abslt  15277  absle  15278  o1lo1  15499  o1co  15548  rlimno1  15616  dvdssub2  16270  lublecllem  18324  f1omvdco2  19423  ptpjpre1  23536  iocopnst  24907  ovolicc2lem4  25487  itg2le  25706  ulmcau  26360  cxpeq0  26642  pntrsumbnd2  27530  abslts  28241  cvcon3  32355  atexch  32452  abfmpeld  32727  r1filimi  35246  noinfepfnregs  35276  wsuclem  36005  btwntriv2  36194  btwnexch3  36202  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  finxpsuclem  37713  isinf2  37721  finixpnum  37926  fin2solem  37927  ltflcei  37929  poimirlem27  37968  itg2addnclem  37992  unirep  38035  prter2  39327  cvrcon3b  39723  fltaccoprm  43073  incssnn0  43143  eldioph4b  43239  fphpdo  43245  pellexlem5  43261  pm14.24  44859  traxext  45404  icceuelpart  47890  prsprel  47941  sprsymrelfolem2  47947  goldbachthlem2  48003  gbegt5  48231  aacllem  50270