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  606  anabsi6  671  mpand  696  2eu3  2655  ralcom2  3340  somo  5569  wereu2  5619  smoel  8291  cfub  10160  cofsmo  10180  grudomon  10729  axpre-sup  11081  leltadd  11623  lemul12b  12001  lbzbi  12875  injresinj  13735  swrdnnn0nd  14608  abslt  15266  absle  15267  o1lo1  15488  o1co  15537  rlimno1  15605  dvdssub2  16259  lublecllem  18313  f1omvdco2  19412  ptpjpre1  23545  iocopnst  24916  ovolicc2lem4  25496  itg2le  25715  ulmcau  26375  cxpeq0  26658  pntrsumbnd2  27549  abslts  28260  cvcon3  32375  atexch  32472  abfmpeld  32747  r1filimi  35267  noinfepfnregs  35297  wsuclem  36026  btwntriv2  36215  btwnexch3  36223  isbasisrelowllem1  37682  isbasisrelowllem2  37683  relowlssretop  37690  finxpsuclem  37724  isinf2  37732  finixpnum  37937  fin2solem  37938  ltflcei  37940  poimirlem27  37979  itg2addnclem  38003  unirep  38046  prter2  39338  cvrcon3b  39734  fltaccoprm  43084  incssnn0  43154  eldioph4b  43254  fphpdo  43260  pellexlem5  43276  pm14.24  44874  traxext  45419  icceuelpart  47893  prsprel  47944  sprsymrelfolem2  47950  goldbachthlem2  48006  gbegt5  48234  aacllem  50273