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  2780  somo  4430  wereu2  4472  ordtr3  4519  ralxfrd  4630  poirr2  5149  smoel  6464  cfub  7965  cofsmo  7985  grudomon  8529  axpre-sup  8881  leltadd  9348  lemul12b  9703  lbzbi  10398  abslt  11894  absle  11895  o1lo1  12107  o1co  12156  rlimno1  12223  znnenlem  12587  dvdssub2  12663  lubid  14215  ptpjpre1  17372  iocopnst  18542  ovolicc2lem4  18983  itg2le  19198  ulmcau  19878  cxpeq0  20136  pntrsumbnd2  20828  cvcon3  22978  atexch  23075  abfmpeld  23269  nofulllem5  24918  btwntriv2  25194  btwnexch3  25202  ltflcei  25485  itg2addnclem  25492  unirep  25673  prter2  26072  incssnn0  26109  eldioph4b  26217  fphpdo  26223  pellexlem5  26241  f1omvdco2  26714  pm14.24  26955  injresinj  27465  a12study3  29204  cvrcon3b  29536
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