Theorem ancomsd 471

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan2d  617  anabsi6  683  mpand  708  2eu3  2678  ralcom2  3362  somo  5597  wereu2  5647  smoel  8369  r1filimi  9904  cfub  10327  cofsmo  10348  grudomon  10903  axpre-sup  11255  leltadd  11801  lemul12b  12175  lbzbi  13064  injresinj  13927  swrdnnn0nd  14807  abslt  15483  absle  15484  o1lo1  15705  o1co  15754  rlimno1  15822  dvdssub2  16472  lublecllem  18533  f1omvdco2  19663  ptpjpre1  23891  iocopnst  25262  ovolicc2lem4  25842  itg2le  26061  ulmcau  26723  cxpeq0  27007  pntrsumbnd2  27895  fltaccoprm  27973  abslts  28636  cvcon3  32887  atexch  32984  abfmpeld  33291  acwer1prclem  35808  noinfepfnregs  35849  wsuclem  36662  btwntriv2  36852  btwnexch3  36860  isbasisrelowllem1  38354  isbasisrelowllem2  38355  relowlssretop  38362  finxpsuclem  38396  isinf2  38404  finixpnum  38604  fin2solem  38605  ltflcei  38607  poimirlem27  38641  itg2addnclem  38665  unirep  38724  prter2  40014  cvrcon3b  40410  incssnn0  43798  eldioph4b  43894  fphpdo  43900  pellexlem5  43916  pm14.24  45492  traxext  46043  icceuelpart  48594  prsprel  48645  sprsymrelfolem2  48651  goldbachthlem2  48707  gbegt5  48935  aacllem  51015