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  605  anabsi6  670  mpand  695  2eu3  2654  ralcom2  3377  somo  5631  wereu2  5682  smoel  8400  cfub  10289  cofsmo  10309  grudomon  10857  axpre-sup  11209  leltadd  11747  lemul12b  12124  lbzbi  12978  injresinj  13827  swrdnnn0nd  14694  abslt  15353  absle  15354  o1lo1  15573  o1co  15622  rlimno1  15690  dvdssub2  16338  lublecllem  18405  f1omvdco2  19466  ptpjpre1  23579  iocopnst  24970  ovolicc2lem4  25555  itg2le  25774  ulmcau  26438  cxpeq0  26720  pntrsumbnd2  27611  absslt  28273  cvcon3  32303  atexch  32400  abfmpeld  32664  wsuclem  35826  btwntriv2  36013  btwnexch3  36021  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  finxpsuclem  37398  isinf2  37406  finixpnum  37612  fin2solem  37613  ltflcei  37615  poimirlem27  37654  itg2addnclem  37678  unirep  37721  prter2  38882  cvrcon3b  39278  fltaccoprm  42650  incssnn0  42722  eldioph4b  42822  fphpdo  42828  pellexlem5  42844  pm14.24  44451  traxext  44994  icceuelpart  47423  prsprel  47474  sprsymrelfolem2  47480  goldbachthlem2  47533  gbegt5  47748  aacllem  49320