Theorem ancomsd 466

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylan2d  611  anabsi6  676  mpand  701  2eu3  2658  ralcom2  3342  somo  5572  wereu2  5622  smoel  8297  cfub  10169  cofsmo  10189  grudomon  10738  axpre-sup  11090  leltadd  11632  lemul12b  12010  lbzbi  12884  injresinj  13744  swrdnnn0nd  14617  abslt  15275  absle  15276  o1lo1  15497  o1co  15546  rlimno1  15614  dvdssub2  16268  lublecllem  18322  f1omvdco2  19421  ptpjpre1  23561  iocopnst  24932  ovolicc2lem4  25512  itg2le  25731  ulmcau  26385  cxpeq0  26667  pntrsumbnd2  27555  abslts  28266  cvcon3  32380  atexch  32477  abfmpeld  32753  r1filimi  35293  noinfepfnregs  35323  wsuclem  36052  btwntriv2  36241  btwnexch3  36249  isbasisrelowllem1  37718  isbasisrelowllem2  37719  relowlssretop  37726  finxpsuclem  37760  isinf2  37768  finixpnum  37973  fin2solem  37974  ltflcei  37976  poimirlem27  38015  itg2addnclem  38039  unirep  38082  prter2  39374  cvrcon3b  39770  fltaccoprm  43091  incssnn0  43161  eldioph4b  43257  fphpdo  43263  pellexlem5  43279  pm14.24  44877  traxext  45422  icceuelpart  47912  prsprel  47963  sprsymrelfolem2  47969  goldbachthlem2  48025  gbegt5  48253  aacllem  50292