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

Theorem sylanb 459
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1  |-  ( ph  <->  ps )
sylanb.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylanb  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3  |-  ( ph  <->  ps )
21biimpi 187 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 458 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anb  466  anabsan  787  eqtr2  2398  pm13.181  2616  rmob  3185  sspsstr  3388  disjne  3609  seex  4479  tron  4538  ordsucss  4731  ordsucelsuc  4735  xpcan2  5239  fssres  5543  funbrfvb  5701  funopfvb  5702  fvco  5731  fvimacnvi  5776  ffvresb  5832  funressn  5851  fvtp2  5872  fvtp2g  5875  fnex  5893  funex  5895  1st2nd  6325  frxp  6385  dftpos4  6427  tz7.48lem  6627  nnmsucr  6797  nnmcan  6806  xpmapenlem  7203  php  7220  php4  7223  omsucdomOLD  7231  isfinite2  7294  wofib  7440  r1limg  7623  r1pwcl  7699  cardmin2  7811  zornn0g  8311  intgru  8615  supsrlem  8912  uzindOLD  10289  fnn0ind  10294  uztrn2  10428  nnwo  10467  irradd  10523  qbtwnxr  10711  xltnegi  10727  xaddnemnf  10745  xaddnepnf  10746  xaddcom  10749  xnegdi  10752  elioore  10871  leexp2  11354  faclbnd  11501  faclbnd3  11503  brfi1uzind  11635  dvdslelem  12814  divalglem1  12834  isprm2lem  13006  dvdsprime  13012  pcgcd  13171  cntri  15049  efgsrel  15286  xrsdsreclb  16661  znf1o  16748  restuni  17141  stoig  17142  restperf  17163  resstps  17166  pnfnei  17199  mnfnei  17200  cnnei  17261  cmpsublem  17377  tx1stc  17596  xkopt  17601  isfcls  17955  tgioo  18691  opnreen  18726  iscmet3  19110  dyaddisj  19348  limcmpt  19630  degltlem1  19855  ulmdvlem3  20178  lgsdi  20976  eupath2lem3  21542  grpoidinvlem3  21635  ipasslem3  22175  spanuni  22887  5oalem3  22999  5oalem5  23001  mdslmd1lem2  23670  mptct  23943  mptctf  23946  xaddeq0  24023  esumcvg  24265  measres  24363  measdivcstOLD  24365  measdivcst  24366  probun  24449  dfon2lem9  25164  noreson  25331  funpartfun  25499  cgrxfr  25696  segcon2  25746  brsegle2  25750  seglecgr12im  25751  segletr  25755  nn0prpw  26010  comppfsc  26071  prtlem11  26399  mzpclall  26468  funbrafvb  27682  funopafvb  27683  afvco2  27702
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