Theorem ancomsd 471

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan2d  617  anabsi6  683  mpand  708  2eu3  2681  ralcom2  3366  somo  5602  wereu2  5652  smoel  8396  r1filimi  9930  cfub  10353  cofsmo  10374  grudomon  10929  axpre-sup  11281  leltadd  11827  lemul12b  12201  lbzbi  13090  injresinj  13953  swrdnnn0nd  14834  abslt  15511  absle  15512  o1lo1  15733  o1co  15782  rlimno1  15850  dvdssub2  16500  lublecllem  18561  f1omvdco2  19692  ptpjpre1  23920  iocopnst  25291  ovolicc2lem4  25871  itg2le  26090  ulmcau  26752  cxpeq0  27036  pntrsumbnd2  27924  fltaccoprm  28002  abslts  28665  cvcon3  32916  atexch  33013  abfmpeld  33320  acwer1prclem  35851  noinfepfnregs  35900  elpssmo  36636  wsuclem  36765  btwntriv2  36955  btwnexch3  36963  isbasisrelowllem1  38470  isbasisrelowllem2  38471  relowlssretop  38478  finxpsuclem  38512  isinf2  38520  finixpnum  38720  fin2solem  38721  ltflcei  38723  poimirlem27  38757  itg2addnclem  38781  unirep  38840  prter2  40130  cvrcon3b  40526  incssnn0  43915  eldioph4b  44011  fphpdo  44017  pellexlem5  44033  pm14.24  45607  traxext  46162  icceuelpart  48723  prsprel  48774  sprsymrelfolem2  48780  goldbachthlem2  48836  gbegt5  49064  aacllem  51219