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

Theorem ancomsd 451
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 448 . 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  479  mpand  668  anabsi6  807  ralcom2  2875  ralxfrd  4494  somo  4662  wereu2  4704  ordtr3  4751  poirr2  5210  smoel  6807  cfub  8406  cofsmo  8426  grudomon  8972  axpre-sup  9324  leltadd  9811  lemul12b  10174  lbzbi  10931  injresinj  11623  abslt  12786  absle  12787  o1lo1  12999  o1co  13048  rlimno1  13115  znnenlem  13477  dvdssub2  13553  lublecllem  15141  f1omvdco2  15934  ptpjpre1  18986  iocopnst  20354  ovolicc2lem4  20845  itg2le  21059  ulmcau  21745  cxpeq0  22008  pntrsumbnd2  22701  cvcon3  25511  atexch  25608  abfmpeld  25793  wsuclem  27609  nofulllem5  27694  btwntriv2  27890  btwnexch3  27898  finixpnum  28258  fin2solem  28259  ltflcei  28263  itg2addnclem  28287  unirep  28450  prter2  28871  incssnn0  28892  eldioph4b  28995  fphpdo  29001  pellexlem5  29019  pm14.24  29531  cvrcon3b  32495
  Copyright terms: Public domain W3C validator