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  2647  ralcom2  3342  somo  5570  wereu2  5620  smoel  8290  cfub  10162  cofsmo  10182  grudomon  10730  axpre-sup  11082  leltadd  11622  lemul12b  11999  lbzbi  12855  injresinj  13709  swrdnnn0nd  14581  abslt  15240  absle  15241  o1lo1  15462  o1co  15511  rlimno1  15579  dvdssub2  16230  lublecllem  18282  f1omvdco2  19345  ptpjpre1  23474  iocopnst  24853  ovolicc2lem4  25437  itg2le  25656  ulmcau  26320  cxpeq0  26603  pntrsumbnd2  27494  absslt  28174  cvcon3  32246  atexch  32343  abfmpeld  32611  wsuclem  35798  btwntriv2  35985  btwnexch3  35993  isbasisrelowllem1  37328  isbasisrelowllem2  37329  relowlssretop  37336  finxpsuclem  37370  isinf2  37378  finixpnum  37584  fin2solem  37585  ltflcei  37587  poimirlem27  37626  itg2addnclem  37650  unirep  37693  prter2  38859  cvrcon3b  39255  fltaccoprm  42613  incssnn0  42684  eldioph4b  42784  fphpdo  42790  pellexlem5  42806  pm14.24  44405  traxext  44951  icceuelpart  47421  prsprel  47472  sprsymrelfolem2  47478  goldbachthlem2  47531  gbegt5  47746  aacllem  49774