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

Theorem sylanb 460
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 188 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 459 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  syl2anb  467  anabsan  788  eqtr2  2456  pm13.181  2679  rmob  3251  sspsstr  3454  disjne  3675  seex  4547  tron  4606  ordsucss  4800  ordsucelsuc  4804  xpcan2  5308  fssres  5612  funbrfvb  5771  funopfvb  5772  fvco  5801  fvimacnvi  5846  ffvresb  5902  funressn  5921  fvtp2  5942  fvtp2g  5945  fnex  5963  funex  5965  1st2nd  6395  frxp  6458  dftpos4  6500  tz7.48lem  6700  nnmsucr  6870  nnmcan  6879  xpmapenlem  7276  php  7293  php4  7296  omsucdomOLD  7304  isfinite2  7367  wofib  7516  r1limg  7699  r1pwcl  7775  cardmin2  7887  zornn0g  8387  intgru  8691  supsrlem  8988  uzindOLD  10366  fnn0ind  10371  uztrn2  10505  nnwo  10544  irradd  10600  qbtwnxr  10788  xltnegi  10804  xaddnemnf  10822  xaddnepnf  10823  xaddcom  10826  xnegdi  10829  elioore  10948  leexp2  11436  faclbnd  11583  faclbnd3  11585  brfi1uzind  11717  dvdslelem  12896  divalglem1  12916  isprm2lem  13088  dvdsprime  13094  pcgcd  13253  cntri  15131  efgsrel  15368  xrsdsreclb  16747  znf1o  16834  restuni  17228  stoig  17229  restperf  17250  resstps  17253  pnfnei  17286  mnfnei  17287  cnnei  17348  cmpsublem  17464  tx1stc  17684  xkopt  17689  isfcls  18043  tgioo  18829  opnreen  18864  iscmet3  19248  dyaddisj  19490  limcmpt  19772  degltlem1  19997  ulmdvlem3  20320  lgsdi  21118  eupath2lem3  21703  grpoidinvlem3  21796  ipasslem3  22336  spanuni  23048  5oalem3  23160  5oalem5  23162  mdslmd1lem2  23831  mptct  24111  mptctf  24114  xaddeq0  24121  esumcvg  24478  measres  24578  measdivcstOLD  24580  measdivcst  24581  probun  24679  dfon2lem9  25420  noreson  25617  funpartfun  25790  cgrxfr  25991  segcon2  26041  brsegle2  26045  seglecgr12im  26046  segletr  26050  ftc1anclem5  26286  ftc1anc  26290  nn0prpw  26328  comppfsc  26389  prtlem11  26717  mzpclall  26786  funbrafvb  27998  funopafvb  27999  afvco2  28018  fzo1fzo0n0  28139  elfzonelfzo  28143  swrdccat3b  28241  2wlkonotv  28397
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 179  df-an 362
  Copyright terms: Public domain W3C validator