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  5594  wereu2  5644  smoel  8346  r1filimi  9876  cfub  10298  cofsmo  10319  grudomon  10874  axpre-sup  11226  leltadd  11770  lemul12b  12144  lbzbi  13033  injresinj  13895  swrdnnn0nd  14774  abslt  15450  absle  15451  o1lo1  15672  o1co  15721  rlimno1  15789  dvdssub2  16439  lublecllem  18494  f1omvdco2  19624  ptpjpre1  23852  iocopnst  25223  ovolicc2lem4  25803  itg2le  26022  ulmcau  26686  cxpeq0  26970  pntrsumbnd2  27858  abslts  28569  cvcon3  32820  atexch  32917  abfmpeld  33182  noinfepfnregs  35725  wsuclem  36509  btwntriv2  36699  btwnexch3  36707  isbasisrelowllem1  38198  isbasisrelowllem2  38199  relowlssretop  38206  finxpsuclem  38240  isinf2  38248  finixpnum  38448  fin2solem  38449  ltflcei  38451  poimirlem27  38485  itg2addnclem  38509  unirep  38568  prter2  39858  cvrcon3b  40254  fltaccoprm  43590  incssnn0  43660  eldioph4b  43756  fphpdo  43762  pellexlem5  43778  pm14.24  45360  traxext  45904  icceuelpart  48440  prsprel  48491  sprsymrelfolem2  48497  goldbachthlem2  48553  gbegt5  48781  aacllem  50861