Theorem ancomsd 470

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan2d  616  anabsi6  682  mpand  707  2eu3  2683  ralcom2  3367  somo  5599  wereu2  5649  smoel  8335  cfub  10220  cofsmo  10241  grudomon  10790  axpre-sup  11142  leltadd  11686  lemul12b  12063  lbzbi  12951  injresinj  13811  swrdnnn0nd  14684  abslt  15356  absle  15357  o1lo1  15578  o1co  15627  rlimno1  15695  dvdssub2  16349  lublecllem  18404  f1omvdco2  19509  ptpjpre1  23689  iocopnst  25060  ovolicc2lem4  25640  itg2le  25859  ulmcau  26516  cxpeq0  26801  pntrsumbnd2  27689  abslts  28400  cvcon3  32545  atexch  32642  abfmpeld  32911  r1filimi  35411  noinfepfnregs  35440  wsuclem  36186  btwntriv2  36375  btwnexch3  36383  isbasisrelowllem1  37861  isbasisrelowllem2  37862  relowlssretop  37869  finxpsuclem  37903  isinf2  37911  finixpnum  38116  fin2solem  38117  ltflcei  38119  poimirlem27  38158  itg2addnclem  38182  unirep  38225  prter2  39517  cvrcon3b  39913  fltaccoprm  43234  incssnn0  43304  eldioph4b  43400  fphpdo  43406  pellexlem5  43422  pm14.24  45006  traxext  45551  icceuelpart  48040  prsprel  48091  sprsymrelfolem2  48097  goldbachthlem2  48153  gbegt5  48381  aacllem  50430