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  2651  ralcom2  3374  somo  5634  wereu2  5685  smoel  8398  cfub  10286  cofsmo  10306  grudomon  10854  axpre-sup  11206  leltadd  11744  lemul12b  12121  lbzbi  12975  injresinj  13823  swrdnnn0nd  14690  abslt  15349  absle  15350  o1lo1  15569  o1co  15618  rlimno1  15686  dvdssub2  16334  lublecllem  18417  f1omvdco2  19480  ptpjpre1  23594  iocopnst  24983  ovolicc2lem4  25568  itg2le  25788  ulmcau  26452  cxpeq0  26734  pntrsumbnd2  27625  absslt  28287  cvcon3  32312  atexch  32409  abfmpeld  32670  wsuclem  35806  btwntriv2  35993  btwnexch3  36001  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  finxpsuclem  37379  isinf2  37387  finixpnum  37591  fin2solem  37592  ltflcei  37594  poimirlem27  37633  itg2addnclem  37657  unirep  37700  prter2  38862  cvrcon3b  39258  fltaccoprm  42626  incssnn0  42698  eldioph4b  42798  fphpdo  42804  pellexlem5  42820  pm14.24  44427  traxext  44937  icceuelpart  47360  prsprel  47411  sprsymrelfolem2  47417  goldbachthlem2  47470  gbegt5  47685  aacllem  49031