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

Theorem sylanb 562
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 206 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 561 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 197  df-an 383
This theorem is referenced by:  syl2anb  577  anabsan  636  eqtr2  2790  pm13.181  3024  rmob  3676  sspsstr  3860  disjne  4163  seex  5212  xpcan2  5712  tron  5889  fssres  6210  funbrfvb  6379  funopfvb  6380  fvco  6416  fvimacnvi  6474  ffvresb  6536  funressn  6568  funresdfunsn  6598  fvtp2  6604  fvtp2g  6607  fnex  6624  funex  6625  ordsucss  7164  ordsucelsuc  7168  1st2nd  7362  frxp  7437  dftpos4  7522  tz7.48lem  7688  nnmsucr  7858  nnmcan  7867  xpmapenlem  8282  php  8299  php4  8302  isfinite2  8373  fundmfibi  8400  fiinfcl  8562  wofib  8605  r1limg  8797  r1pwcl  8873  cardmin2  9023  zornn0g  9528  mptct  9561  intgru  9837  supsrlem  10133  nzadd  11626  fnn0ind  11677  uztrn2  11905  nnwo  11955  irradd  12014  qbtwnxr  12235  xltnegi  12251  xaddnemnf  12271  xaddnepnf  12272  xaddcom  12275  xnegdi  12282  elioore  12409  uzsubsubfz1  12570  fzo1fzo0n0  12726  elfzonelfzo  12777  modsumfzodifsn  12950  leexp2  13121  faclbnd  13280  faclbnd3  13282  fi1uzind  13480  brfi1uzind  13481  opfi1uzind  13484  swrdccat3b  13704  dvdslelem  15239  divalglem1  15324  dvdsprime  15606  pcgcd  15788  cntri  17969  efgsrel  18353  xrsdsreclb  20007  znf1o  20114  restuni  21186  stoig  21187  restperf  21208  resstps  21211  pnfnei  21244  mnfnei  21245  cnnei  21306  cmpsublem  21422  comppfsc  21555  tx1stc  21673  xkopt  21678  isfcls  22032  tgioo  22818  opnreen  22853  iscmet3  23309  dyaddisj  23583  limcmpt  23866  degltlem1  24051  ulmdvlem3  24375  lgsdi  25279  cusgrres  26578  crctcshwlkn0lem4  26940  crctcshwlkn0lem5  26941  wwlksnred  27034  clwlksfclwwlkOLD  27240  eupth2lem3lem4  27408  grpoidinvlem3  27694  ipasslem3  28022  spanuni  28737  5oalem3  28849  5oalem5  28851  mdslmd1lem2  29519  mptctf  29829  xaddeq0  29852  ordtconnlem1  30304  esumcvg  30482  ldgenpisyslem1  30560  measres  30619  measdivcstOLD  30621  measdivcst  30622  probun  30815  elmpps  31802  dfon2lem9  32026  noreson  32144  funpartfun  32381  cgrxfr  32493  segcon2  32543  brsegle2  32547  seglecgr12im  32548  segletr  32552  nn0prpw  32649  bj-seex  33244  lindsenlbs  33730  matunitlindflem2  33732  ptrecube  33735  poimirlem28  33763  ftc1anclem5  33814  ftc1anc  33818  exlimddvfi  34252  prtlem11  34667  mzpclall  37809  4an31  39223  cnrefiisplem  40567  iundjiun  41188  funbrafvb  41750  funopafvb  41751  afvco2  41770  sprsymrelfolem2  42261
  Copyright terms: Public domain W3C validator