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

Theorem sylanb 458
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 186 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 457 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  syl2anb  465  anabsan  786  eqtr2  2314  pm13.181  2532  rmob  3092  sspsstr  3294  disjne  3513  seex  4372  tron  4431  ordsucss  4625  ordsucelsuc  4629  xpcan2  5129  fssres  5424  funbrfvb  5581  funopfvb  5582  fvco  5611  fvimacnvi  5655  ffvresb  5706  funressn  5722  fvtp2  5741  fnex  5757  funex  5759  1st2nd  6182  frxp  6241  dftpos4  6269  tz7.48lem  6469  nnmsucr  6639  nnmcan  6648  xpmapenlem  7044  php  7061  php4  7064  omsucdomOLD  7072  isfinite2  7131  wofib  7276  r1limg  7459  r1pwcl  7535  cardmin2  7647  zornn0g  8148  intgru  8452  supsrlem  8749  uzindOLD  10122  fnn0ind  10127  uztrn2  10261  nnwo  10300  irradd  10356  qbtwnxr  10543  xltnegi  10559  xaddnemnf  10577  xaddnepnf  10578  xaddcom  10581  xnegdi  10584  elioore  10702  leexp2  11172  faclbnd  11319  faclbnd3  11321  dvdslelem  12589  divalglem1  12609  isprm2lem  12781  dvdsprime  12787  pcgcd  12946  cntri  14822  efgsrel  15059  xrsdsreclb  16434  znf1o  16521  restuni  16909  stoig  16910  restperf  16930  resstps  16933  pnfnei  16966  mnfnei  16967  cmpsublem  17142  tx1stc  17360  xkopt  17365  isfcls  17720  tgioo  18318  opnreen  18352  iscmet3  18735  dyaddisj  18967  limcmpt  19249  degltlem1  19474  ulmdvlem3  19795  lgsdi  20587  grpoidinvlem3  20889  ipasslem3  21427  spanuni  22139  5oalem3  22251  5oalem5  22253  mdslmd1lem2  22922  xaddeq0  23319  mptct  23360  mptctf  23363  esumcvg  23469  measres  23564  measdivcstOLD  23566  measdivcst  23567  probun  23637  eupath2lem3  23918  dfon2lem9  24218  noreson  24385  funpartfun  24553  cgrxfr  24750  segcon2  24800  brsegle2  24804  seglecgr12im  24805  segletr  24809  clfsebs  25450  trinv  25498  plimfil  25661  limfilnei  25664  cnegvex2  25763  rnegvex2  25764  clsmulrv  25786  nn0prpw  26342  connsubOLD  26357  comppfsc  26410  prtlem11  26837  mzpclall  26908  funbrafvb  28124  funopafvb  28125  afvco2  28144
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 177  df-an 360
  Copyright terms: Public domain W3C validator