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

Theorem sylanb 581
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 217 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 580 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  syl2anb  597  anabsan  661  eqtr2  2842  pm13.181  3099  rmob  3873  sspsstr  4081  disjne  4402  rexopabb  5407  seex  5512  xpcan2  6028  tron  6208  fssres  6538  funbrfvb  6714  funopfvb  6715  fvco  6753  fvimacnvi  6815  ffvresb  6881  funressn  6914  funresdfunsn  6944  fvtp2  6951  fvtp2g  6954  fnex  6972  funex  6974  ordsucss  7521  ordsucelsuc  7525  1st2nd  7729  1stconst  7786  2ndconst  7787  frxp  7811  imacosupp  7865  dftpos4  7902  tz7.48lem  8068  nnmsucr  8241  nnmcan  8250  xpmapenlem  8673  php  8690  php4  8693  isfinite2  8765  fundmfibi  8792  fiinfcl  8954  wofib  8998  r1limg  9189  r1pwcl  9265  cardmin2  9416  zornn0g  9916  mptct  9949  intgru  10225  supsrlem  10522  nzadd  12019  fnn0ind  12070  uztrn2  12251  nnwo  12302  irradd  12362  qbtwnxr  12583  xltnegi  12599  xaddnemnf  12619  xaddnepnf  12620  xaddcom  12623  xnegdi  12631  elioore  12758  uzsubsubfz1  12920  fzo1fzo0n0  13078  elfzonelfzo  13129  modsumfzodifsn  13302  leexp2  13525  faclbnd  13640  faclbnd3  13642  fi1uzind  13845  brfi1uzind  13846  opfi1uzind  13849  swrdccat3b  14092  dvdslelem  15649  divalglem1  15735  dvdsprime  16021  pcgcd  16204  cntri  18401  efgsrel  18791  xrsdsreclb  20522  znf1o  20628  restuni  21700  stoig  21701  restperf  21722  resstps  21725  pnfnei  21758  mnfnei  21759  cnnei  21820  cmpsublem  21937  comppfsc  22070  tx1stc  22188  xkopt  22193  isfcls  22547  tgioo  23333  opnreen  23368  iscmet3  23825  dyaddisj  24126  limcmpt  24410  degltlem1  24595  ulmdvlem3  24919  lgsdi  25838  cusgrres  27158  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  wwlksnred  27598  eupth2lem3lem4  27938  grpoidinvlem3  28211  ipasslem3  28538  spanuni  29249  5oalem3  29361  5oalem5  29363  mdslmd1lem2  30031  mptctf  30380  xaddeq0  30404  xnn0gt0  30421  ordtconnlem1  31067  esumcvg  31245  ldgenpisyslem1  31322  measres  31381  measdivcst  31383  measdivcstALTV  31384  probun  31577  elmpps  32718  dfon2lem9  32934  noreson  33065  funpartfun  33302  cgrxfr  33414  segcon2  33464  brsegle2  33468  seglecgr12im  33469  segletr  33473  nn0prpw  33569  bj-seex  34139  fvineqsneu  34575  lindsenlbs  34769  matunitlindflem2  34771  ptrecube  34774  poimirlem28  34802  ftc1anclem5  34853  ftc1anc  34857  exlimddvfi  35283  mzpclall  39204  4an31  40712  cnrefiisplem  41990  iundjiun  42623  funbrafvb  43236  funopafvb  43237  afvco2  43256  dfatbrafv2b  43325  funbrafv22b  43330  funopafv2b  43331  sprsymrelfolem2  43502  line2xlem  44638  itsclc0xyqsol  44653  setrec2lem2  44695
  Copyright terms: Public domain W3C validator