Theorem ancomsd 470

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 466	. 2 |- ( ( ch /\ ps ) <-> ( ps /\ ch ) )
2		ancomsd.1	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	1, 2	syl5bi 232	1 |- ( ph -> ( ( ch /\ ps ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  sylan2d  499  mpand  711  anabsi6  859  ralcom2  3104  ralxfrdOLD  4880  somo  5069  wereu2  5111  poirr2  5520  smoel  7457  cfub  9071  cofsmo  9091  grudomon  9639  axpre-sup  9990  leltadd  10512  lemul12b  10880  lbzbi  11776  injresinj  12589  abslt  14054  absle  14055  o1lo1  14268  o1co  14317  rlimno1  14384  znnenlem  14940  dvdssub2  15023  lublecllem  16988  f1omvdco2  17868  ptpjpre1  21374  iocopnst  22739  ovolicc2lem4  23288  itg2le  23506  ulmcau  24149  cxpeq0  24424  pntrsumbnd2  25256  cvcon3  29143  atexch  29240  abfmpeld  29454  wsuclem  31773  wsuclemOLD  31774  btwntriv2  32119  btwnexch3  32127  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  finxpsuclem  33234  finixpnum  33394  fin2solem  33395  ltflcei  33397  poimirlem27  33436  itg2addnclem  33461  unirep  33507  prter2  34166  cvrcon3b  34564  incssnn0  37274  eldioph4b  37375  fphpdo  37381  pellexlem5  37397  pm14.24  38633  icceuelpart  41372  goldbachthlem2  41458  gbegt5  41649  prsprel  41737  sprsymrelfolem2  41743  aacllem  42547