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  818  ralcom2  3022  ralxfrd  4670  somo  4843  wereu2  4885  ordtr3  4932  poirr2  5401  smoel  7049  cfub  8646  cofsmo  8666  grudomon  9212  axpre-sup  9563  leltadd  10057  lemul12b  10420  lbzbi  11195  injresinj  11929  abslt  13159  absle  13160  o1lo1  13372  o1co  13421  rlimno1  13488  znnenlem  13957  dvdssub2  14035  lublecllem  15745  f1omvdco2  16600  ptpjpre1  20198  iocopnst  21566  ovolicc2lem4  22057  itg2le  22272  ulmcau  22916  cxpeq0  23185  pntrsumbnd2  23878  cvcon3  27330  atexch  27427  abfmpeld  27640  wsuclem  29577  nofulllem5  29662  btwntriv2  29846  btwnexch3  29854  finixpnum  30222  fin2solem  30223  ltflcei  30227  itg2addnclem  30250  unirep  30387  prter2  30806  incssnn0  30827  eldioph4b  30928  fphpdo  30934  pellexlem5  30952  pm14.24  31522  aacllem  33339  cvrcon3b  35124