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  853  eqtr2  2641  pm13.181  2872  rmob  3514  sspsstr  3695  disjne  3999  seex  5042  xpcan2  5535  tron  5710  fssres  6032  funbrfvb  6200  funopfvb  6201  fvco  6236  fvimacnvi  6292  ffvresb  6355  funressn  6386  funresdfunsn  6415  fvtp2  6421  fvtp2g  6424  fnex  6441  funex  6442  ordsucss  6972  ordsucelsuc  6976  1st2nd  7166  frxp  7239  dftpos4  7323  tz7.48lem  7488  nnmsucr  7657  nnmcan  7666  xpmapenlem  8078  php  8095  php4  8098  isfinite2  8169  fundmfibi  8196  fiinfcl  8358  wofib  8401  r1limg  8585  r1pwcl  8661  cardmin2  8775  zornn0g  9278  mptct  9311  intgru  9587  supsrlem  9883  nzadd  11376  fnn0ind  11427  uztrn2  11656  nnwo  11704  irradd  11763  qbtwnxr  11981  xltnegi  11997  xaddnemnf  12017  xaddnepnf  12018  xaddcom  12021  xnegdi  12028  elioore  12154  uzsubsubfz1  12313  fzo1fzo0n0  12466  elfzonelfzo  12518  modsumfzodifsn  12690  leexp2  12862  faclbnd  13024  faclbnd3  13026  fi1uzind  13225  brfi1uzind  13226  opfi1uzind  13229  fi1uzindOLD  13231  brfi1uzindOLD  13232  opfi1uzindOLD  13235  swrdccat3b  13440  dvdslelem  14962  divalglem1  15048  isprm2lem  15325  dvdsprime  15331  pcgcd  15513  cntri  17691  efgsrel  18075  xrsdsreclb  19721  znf1o  19828  restuni  20885  stoig  20886  restperf  20907  resstps  20910  pnfnei  20943  mnfnei  20944  cnnei  21005  cmpsublem  21121  comppfsc  21254  tx1stc  21372  xkopt  21377  isfcls  21732  tgioo  22518  opnreen  22553  iscmet3  23010  dyaddisj  23283  limcmpt  23566  degltlem1  23749  ulmdvlem3  24073  lgsdi  24972  cusgrres  26244  crctcshwlkn0lem4  26587  crctcshwlkn0lem5  26588  wwlksnred  26669  clwlksfclwwlk  26841  eupth2lem3lem4  26970  grpoidinvlem3  27227  ipasslem3  27555  spanuni  28270  5oalem3  28382  5oalem5  28384  mdslmd1lem2  29052  mptctf  29356  xaddeq0  29379  ordtconnlem1  29770  esumcvg  29947  ldgenpisyslem1  30025  measres  30084  measdivcstOLD  30086  measdivcst  30087  probun  30280  elmpps  31205  dfon2lem9  31424  noreson  31541  funpartfun  31719  cgrxfr  31831  segcon2  31881  brsegle2  31885  seglecgr12im  31886  segletr  31890  nn0prpw  31987  bj-seex  32593  lindsenlbs  33063  matunitlindflem2  33065  ptrecube  33068  poimirlem28  33096  ftc1anclem5  33148  ftc1anc  33152  exlimddvfi  33586  prtlem11  33658  mzpclall  36797  4an31  38213  iundjiun  40005  funbrafvb  40561  funopafvb  40562  afvco2  40581  sprsymrelfolem2  41052
  Copyright terms: Public domain W3C validator