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

Theorem sylanb 489
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 488 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  syl2anb  496  anabsan  854  eqtr2  2641  pm13.181  2875  rmob  3527  sspsstr  3710  disjne  4020  seex  5075  xpcan2  5569  tron  5744  fssres  6068  funbrfvb  6236  funopfvb  6237  fvco  6272  fvimacnvi  6329  ffvresb  6392  funressn  6423  funresdfunsn  6452  fvtp2  6458  fvtp2g  6461  fnex  6478  funex  6479  ordsucss  7015  ordsucelsuc  7019  1st2nd  7211  frxp  7284  dftpos4  7368  tz7.48lem  7533  nnmsucr  7702  nnmcan  7711  xpmapenlem  8124  php  8141  php4  8144  isfinite2  8215  fundmfibi  8242  fiinfcl  8404  wofib  8447  r1limg  8631  r1pwcl  8707  cardmin2  8821  zornn0g  9324  mptct  9357  intgru  9633  supsrlem  9929  nzadd  11422  fnn0ind  11473  uztrn2  11702  nnwo  11750  irradd  11809  qbtwnxr  12028  xltnegi  12044  xaddnemnf  12064  xaddnepnf  12065  xaddcom  12068  xnegdi  12075  elioore  12202  uzsubsubfz1  12361  fzo1fzo0n0  12514  elfzonelfzo  12566  modsumfzodifsn  12738  leexp2  12910  faclbnd  13072  faclbnd3  13074  fi1uzind  13274  brfi1uzind  13275  opfi1uzind  13278  fi1uzindOLD  13280  brfi1uzindOLD  13281  opfi1uzindOLD  13284  swrdccat3b  13490  dvdslelem  15025  divalglem1  15111  isprm2lem  15388  dvdsprime  15394  pcgcd  15576  cntri  17757  efgsrel  18141  xrsdsreclb  19787  znf1o  19894  restuni  20960  stoig  20961  restperf  20982  resstps  20985  pnfnei  21018  mnfnei  21019  cnnei  21080  cmpsublem  21196  comppfsc  21329  tx1stc  21447  xkopt  21452  isfcls  21807  tgioo  22593  opnreen  22628  iscmet3  23085  dyaddisj  23358  limcmpt  23641  degltlem1  23826  ulmdvlem3  24150  lgsdi  25053  cusgrres  26338  crctcshwlkn0lem4  26699  crctcshwlkn0lem5  26700  wwlksnred  26781  clwlksfclwwlk  26955  eupth2lem3lem4  27084  grpoidinvlem3  27344  ipasslem3  27672  spanuni  28387  5oalem3  28499  5oalem5  28501  mdslmd1lem2  29169  mptctf  29480  xaddeq0  29503  ordtconnlem1  29955  esumcvg  30133  ldgenpisyslem1  30211  measres  30270  measdivcstOLD  30272  measdivcst  30273  probun  30466  elmpps  31455  dfon2lem9  31680  noreson  31797  funpartfun  32034  cgrxfr  32146  segcon2  32196  brsegle2  32200  seglecgr12im  32201  segletr  32205  nn0prpw  32302  bj-seex  32903  lindsenlbs  33384  matunitlindflem2  33386  ptrecube  33389  poimirlem28  33417  ftc1anclem5  33469  ftc1anc  33473  exlimddvfi  33907  prtlem11  33977  mzpclall  37116  4an31  38530  iundjiun  40446  funbrafvb  41005  funopafvb  41006  afvco2  41025  sprsymrelfolem2  41514
  Copyright terms: Public domain W3C validator