MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancomsd Unicode version

Theorem ancomsd 440
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
StepHypRef Expression
1 ancom 437 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
2 ancomsd.1 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
31, 2syl5bi 208 1  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylan2d  468  mpand  656  anabsi6  791  ralcom2  2704  somo  4348  wereu2  4390  ordtr3  4437  ralxfrd  4548  poirr2  5067  smoel  6377  cfub  7875  cofsmo  7895  grudomon  8439  axpre-sup  8791  leltadd  9258  lemul12b  9613  lbzbi  10306  abslt  11798  absle  11799  o1lo1  12011  o1co  12060  rlimno1  12127  znnenlem  12490  dvdssub2  12566  lubid  14116  ptpjpre1  17266  iocopnst  18438  ovolicc2lem4  18879  itg2le  19094  ulmcau  19772  cxpeq0  20025  pntrsumbnd2  20716  cvcon3  22864  atexch  22961  abfmpeld  23218  nofulllem5  24360  btwntriv2  24635  btwnexch3  24643  setiscat  25979  unirep  26349  prter2  26749  incssnn0  26786  eldioph4b  26894  fphpdo  26900  pellexlem5  26918  f1omvdco2  27391  pm14.24  27632  a12study3  29135  cvrcon3b  29467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator