Theorem ancomsd 454

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

Hypothesis

Ref	Expression
ancomsd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
ancomsd	|- ( ph -> ( ( ch /\ ps ) -> th ) )

Proof of Theorem ancomsd

Step	Hyp	Ref	Expression
1		ancom 450	. 2 |- ( ( ch /\ ps ) <-> ( ps /\ ch ) )
2		ancomsd.1	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	1, 2	syl5bi 217	1 |- ( ph -> ( ( ch /\ ps ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sylan2d  482  mpand  675  anabsi6  814  ralcom2  2991  ralxfrd  4617  somo  4786  wereu2  4828  ordtr3  4875  poirr2  5333  smoel  6934  cfub  8533  cofsmo  8553  grudomon  9099  axpre-sup  9451  leltadd  9938  lemul12b  10301  lbzbi  11058  injresinj  11760  abslt  12924  absle  12925  o1lo1  13137  o1co  13186  rlimno1  13253  znnenlem  13616  dvdssub2  13692  lublecllem  15281  f1omvdco2  16077  ptpjpre1  19286  iocopnst  20654  ovolicc2lem4  21145  itg2le  21360  ulmcau  22003  cxpeq0  22266  pntrsumbnd2  22959  cvcon3  25867  atexch  25964  abfmpeld  26147  wsuclem  27929  nofulllem5  28014  btwntriv2  28210  btwnexch3  28218  finixpnum  28585  fin2solem  28586  ltflcei  28590  itg2addnclem  28614  unirep  28777  prter2  29197  incssnn0  29218  eldioph4b  29321  fphpdo  29327  pellexlem5  29345  pm14.24  29857  cvrcon3b  33285