Theorem ancomsd 468

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylan2d  613  anabsi6  678  mpand  703  2eu3  2674  ralcom2  3358  somo  5587  wereu2  5637  smoel  8319  cfub  10195  cofsmo  10216  grudomon  10765  axpre-sup  11117  leltadd  11661  lemul12b  12038  lbzbi  12927  injresinj  13787  swrdnnn0nd  14660  abslt  15318  absle  15319  o1lo1  15540  o1co  15589  rlimno1  15657  dvdssub2  16311  lublecllem  18366  f1omvdco2  19464  ptpjpre1  23604  iocopnst  24975  ovolicc2lem4  25555  itg2le  25774  ulmcau  26428  cxpeq0  26713  pntrsumbnd2  27601  abslts  28312  cvcon3  32426  atexch  32523  abfmpeld  32799  r1filimi  35354  noinfepfnregs  35383  wsuclem  36121  btwntriv2  36310  btwnexch3  36318  isbasisrelowllem1  37797  isbasisrelowllem2  37798  relowlssretop  37805  finxpsuclem  37839  isinf2  37847  finixpnum  38052  fin2solem  38053  ltflcei  38055  poimirlem27  38094  itg2addnclem  38118  unirep  38161  prter2  39453  cvrcon3b  39849  fltaccoprm  43170  incssnn0  43240  eldioph4b  43336  fphpdo  43342  pellexlem5  43358  pm14.24  44956  traxext  45501  icceuelpart  47990  prsprel  48041  sprsymrelfolem2  48047  goldbachthlem2  48103  gbegt5  48331  aacllem  50370