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 206  df-an 396

This theorem is referenced by:  sylan2d  604  anabsi6  667  mpand  692  2eu3  2641  ralcom2  3365  somo  5615  wereu2  5663  smoel  8355  cfub  10239  cofsmo  10259  grudomon  10807  axpre-sup  11159  leltadd  11694  lemul12b  12067  lbzbi  12916  injresinj  13749  swrdnnn0nd  14602  abslt  15257  absle  15258  o1lo1  15477  o1co  15526  rlimno1  15596  dvdssub2  16240  lublecllem  18312  f1omvdco2  19353  ptpjpre1  23385  iocopnst  24774  ovolicc2lem4  25359  itg2le  25579  ulmcau  26236  cxpeq0  26516  pntrsumbnd2  27404  absslt  28047  cvcon3  31961  atexch  32058  abfmpeld  32303  wsuclem  35258  btwntriv2  35445  btwnexch3  35453  isbasisrelowllem1  36692  isbasisrelowllem2  36693  relowlssretop  36700  finxpsuclem  36734  isinf2  36742  finixpnum  36929  fin2solem  36930  ltflcei  36932  poimirlem27  36971  itg2addnclem  36995  unirep  37038  prter2  38207  cvrcon3b  38603  sn-negex12  41744  fltaccoprm  41837  incssnn0  41904  eldioph4b  42004  fphpdo  42010  pellexlem5  42026  pm14.24  43646  icceuelpart  46555  prsprel  46606  sprsymrelfolem2  46612  goldbachthlem2  46665  gbegt5  46880  aacllem  48002