MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancomsd Structured version   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  2872  somo  4537  wereu2  4579  ordtr3  4626  ralxfrd  4737  poirr2  5258  smoel  6622  cfub  8129  cofsmo  8149  grudomon  8692  axpre-sup  9044  leltadd  9512  lemul12b  9867  lbzbi  10564  injresinj  11200  abslt  12118  absle  12119  o1lo1  12331  o1co  12380  rlimno1  12447  znnenlem  12811  dvdssub2  12887  lubid  14439  ptpjpre1  17603  iocopnst  18965  ovolicc2lem4  19416  itg2le  19631  ulmcau  20311  cxpeq0  20569  pntrsumbnd2  21261  cvcon3  23787  atexch  23884  abfmpeld  24066  wsuclem  25576  nofulllem5  25661  btwntriv2  25946  btwnexch3  25954  ltflcei  26239  itg2addnclem  26256  unirep  26414  prter2  26730  incssnn0  26765  eldioph4b  26872  fphpdo  26878  pellexlem5  26896  f1omvdco2  27368  pm14.24  27609  cvrcon3b  30075
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