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

Theorem ancomsd 454
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 450 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
2 ancomsd.1 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
31, 2syl5bi 217 1  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  sylan2d  482  mpand  675  anabsi6  818  ralcom2  3022  ralxfrd  4670  somo  4843  wereu2  4885  ordtr3  4932  poirr2  5401  smoel  7049  cfub  8646  cofsmo  8666  grudomon  9212  axpre-sup  9563  leltadd  10057  lemul12b  10420  lbzbi  11195  injresinj  11929  abslt  13159  absle  13160  o1lo1  13372  o1co  13421  rlimno1  13488  znnenlem  13957  dvdssub2  14035  lublecllem  15745  f1omvdco2  16600  ptpjpre1  20198  iocopnst  21566  ovolicc2lem4  22057  itg2le  22272  ulmcau  22916  cxpeq0  23185  pntrsumbnd2  23878  cvcon3  27330  atexch  27427  abfmpeld  27640  wsuclem  29577  nofulllem5  29662  btwntriv2  29846  btwnexch3  29854  finixpnum  30222  fin2solem  30223  ltflcei  30227  itg2addnclem  30250  unirep  30387  prter2  30806  incssnn0  30827  eldioph4b  30928  fphpdo  30934  pellexlem5  30952  pm14.24  31522  aacllem  33339  cvrcon3b  35124
  Copyright terms: Public domain W3C validator