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

Theorem sylanb 472
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1
sylanb.2
Assertion
Ref Expression
sylanb

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3
21biimpi 194 . 2
3 sylanb.2 . 2
42, 3sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  syl2anb  479  anabsan  813  eqtr2  2484  pm13.181  2769  rmob  3430  sspsstr  3608  disjne  3872  seex  4847  tron  4906  xpcan2  5449  fssres  5756  funbrfvb  5915  funopfvb  5916  fvco  5949  fvimacnvi  6001  ffvresb  6062  funressn  6084  funresdfunsn  6113  fvtp2  6119  fvtp2g  6122  fnex  6139  funex  6140  ordsucss  6653  ordsucelsuc  6657  1st2nd  6846  frxp  6910  dftpos4  6993  tz7.48lem  7125  nnmsucr  7293  nnmcan  7302  xpmapenlem  7704  php  7721  php4  7724  omsucdomOLD  7733  isfinite2  7798  wofib  7991  r1limg  8210  r1pwcl  8286  cardmin2  8400  zornn0g  8906  intgru  9213  supsrlem  9509  uzindOLD  10982  fnn0ind  10988  uztrn2  11127  nnwo  11176  irradd  11235  qbtwnxr  11428  xltnegi  11444  xaddnemnf  11462  xaddnepnf  11463  xaddcom  11466  xnegdi  11469  elioore  11588  uzsubsubfz1  11737  fzo1fzo0n0  11864  elfzonelfzo  11912  leexp2  12220  faclbnd  12368  faclbnd3  12370  brfi1uzind  12532  swrdccat3b  12721  dvdslelem  14030  divalglem1  14052  isprm2lem  14224  dvdsprime  14230  pcgcd  14401  cntri  16368  efgsrel  16752  xrsdsreclb  18465  znf1o  18590  restuni  19663  stoig  19664  restperf  19685  resstps  19688  pnfnei  19721  mnfnei  19722  cnnei  19783  cmpsublem  19899  comppfsc  20033  tx1stc  20151  xkopt  20156  isfcls  20510  tgioo  21301  opnreen  21336  iscmet3  21732  dyaddisj  22005  limcmpt  22287  degltlem1  22472  ulmdvlem3  22797  lgsdi  23607  clwlkfclwwlk  24844  2wlkonotv  24877  eupath2lem3  24979  grpoidinvlem3  25208  ipasslem3  25748  spanuni  26462  5oalem3  26574  5oalem5  26576  mdslmd1lem2  27245  mptct  27541  mptctf  27544  xaddeq0  27573  ordtconlem1  27906  esumcvg  28092  measres  28193  measdivcstOLD  28195  measdivcst  28196  probun  28358  elmpps  28933  dfon2lem9  29223  noreson  29420  funpartfun  29593  cgrxfr  29705  segcon2  29755  brsegle2  29759  seglecgr12im  29760  segletr  29764  ftc1anclem5  30094  ftc1anc  30098  nn0prpw  30141  exlimddvfi  30527  prtlem11  30607  mzpclall  30659  funbrafvb  32241  funopafvb  32242  afvco2  32261  fundmfibi  32311  usgfis  32446  usgfisALT  32450  4an31  33267  bj-seex  34491
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
  Copyright terms: Public domain W3C validator