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  3348  somo  5572  wereu2  5622  smoel  8294  cfub  10163  cofsmo  10183  grudomon  10732  axpre-sup  11084  leltadd  11625  lemul12b  12002  lbzbi  12853  injresinj  13711  swrdnnn0nd  14584  abslt  15242  absle  15243  o1lo1  15464  o1co  15513  rlimno1  15581  dvdssub2  16232  lublecllem  18285  f1omvdco2  19381  ptpjpre1  23519  iocopnst  24897  ovolicc2lem4  25481  itg2le  25700  ulmcau  26364  cxpeq0  26647  pntrsumbnd2  27538  absslt  28230  cvcon3  32342  atexch  32439  abfmpeld  32714  r1filimi  35240  noinfepfnregs  35269  wsuclem  35998  btwntriv2  36187  btwnexch3  36195  isbasisrelowllem1  37531  isbasisrelowllem2  37532  relowlssretop  37539  finxpsuclem  37573  isinf2  37581  finixpnum  37777  fin2solem  37778  ltflcei  37780  poimirlem27  37819  itg2addnclem  37843  unirep  37886  prter2  39178  cvrcon3b  39574  fltaccoprm  42919  incssnn0  42989  eldioph4b  43089  fphpdo  43095  pellexlem5  43111  pm14.24  44709  traxext  45254  icceuelpart  47718  prsprel  47769  sprsymrelfolem2  47775  goldbachthlem2  47828  gbegt5  48043  aacllem  50082