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  604  anabsi6  669  mpand  694  2eu3  2657  ralcom2  3385  somo  5646  wereu2  5697  smoel  8416  cfub  10318  cofsmo  10338  grudomon  10886  axpre-sup  11238  leltadd  11774  lemul12b  12151  lbzbi  13001  injresinj  13838  swrdnnn0nd  14704  abslt  15363  absle  15364  o1lo1  15583  o1co  15632  rlimno1  15702  dvdssub2  16349  lublecllem  18430  f1omvdco2  19490  ptpjpre1  23600  iocopnst  24989  ovolicc2lem4  25574  itg2le  25794  ulmcau  26456  cxpeq0  26738  pntrsumbnd2  27629  absslt  28291  cvcon3  32316  atexch  32413  abfmpeld  32672  wsuclem  35789  btwntriv2  35976  btwnexch3  35984  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  finxpsuclem  37363  isinf2  37371  finixpnum  37565  fin2solem  37566  ltflcei  37568  poimirlem27  37607  itg2addnclem  37631  unirep  37674  prter2  38837  cvrcon3b  39233  fltaccoprm  42595  incssnn0  42667  eldioph4b  42767  fphpdo  42773  pellexlem5  42789  pm14.24  44401  traxext  44910  icceuelpart  47310  prsprel  47361  sprsymrelfolem2  47367  goldbachthlem2  47420  gbegt5  47635  aacllem  48895