Theorem ancomsd 455

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  sylan2d  484  mpand  679  anabsi6  825  ralcom2  3000  ralxfrd  4636  somo  4809  wereu2  4851  poirr2  5244  ordtr3  5487  smoel  7087  cfub  8677  cofsmo  8697  grudomon  9241  axpre-sup  9592  leltadd  10097  lemul12b  10461  lbzbi  11252  injresinj  12022  abslt  13356  absle  13357  o1lo1  13579  o1co  13628  rlimno1  13695  znnenlem  14242  dvdssub2  14320  lublecllem  16185  f1omvdco2  17040  ptpjpre1  20517  iocopnst  21864  ovolicc2lem4  22351  itg2le  22574  ulmcau  23215  cxpeq0  23488  pntrsumbnd2  24268  cvcon3  27772  atexch  27869  abfmpeld  28093  wsuclem  30295  nofulllem5  30380  btwntriv2  30564  btwnexch3  30572  isbasisrelowllem1  31492  isbasisrelowllem2  31493  relowlssretop  31500  finixpnum  31634  fin2solem  31635  ltflcei  31637  poimirlem27  31671  itg2addnclem  31697  unirep  31743  prter2  32161  cvrcon3b  32552  incssnn0  35262  eldioph4b  35363  fphpdo  35369  pellexlem5  35387  pm14.24  36420  icceuelpart  38140  gbegt5  38252  aacllem  39301