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

Theorem ancomsd 441
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 438 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
2 ancomsd.1 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
31, 2syl5bi 209 1  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylan2d  469  mpand  657  anabsi6  792  ralcom2  2840  somo  4505  wereu2  4547  ordtr3  4594  ralxfrd  4704  poirr2  5225  smoel  6589  cfub  8093  cofsmo  8113  grudomon  8656  axpre-sup  9008  leltadd  9476  lemul12b  9831  lbzbi  10528  injresinj  11163  abslt  12081  absle  12082  o1lo1  12294  o1co  12343  rlimno1  12410  znnenlem  12774  dvdssub2  12850  lubid  14402  ptpjpre1  17564  iocopnst  18926  ovolicc2lem4  19377  itg2le  19592  ulmcau  20272  cxpeq0  20530  pntrsumbnd2  21222  cvcon3  23748  atexch  23845  abfmpeld  24027  nofulllem5  25582  btwntriv2  25858  btwnexch3  25866  ltflcei  26148  itg2addnclem  26163  unirep  26312  prter2  26628  incssnn0  26663  eldioph4b  26770  fphpdo  26776  pellexlem5  26794  f1omvdco2  27267  pm14.24  27508  cvrcon3b  29772
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 178  df-an 361
  Copyright terms: Public domain W3C validator