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

Theorem sylanb 570
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 569 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  585  anabsan  644  eqtr2  2791  pm13.181  3025  rmob  3678  sspsstr  3862  disjne  4165  seex  5212  xpcan2  5712  tron  5889  fssres  6210  funbrfvb  6379  funopfvb  6380  fvco  6416  fvimacnvi  6474  ffvresb  6536  funressn  6569  funresdfunsn  6599  fvtp2  6605  fvtp2g  6608  fnex  6625  funex  6626  ordsucss  7165  ordsucelsuc  7169  1st2nd  7363  frxp  7438  dftpos4  7523  tz7.48lem  7689  nnmsucr  7859  nnmcan  7868  xpmapenlem  8283  php  8300  php4  8303  isfinite2  8374  fundmfibi  8401  fiinfcl  8563  wofib  8606  r1limg  8798  r1pwcl  8874  cardmin2  9024  zornn0g  9529  mptct  9562  intgru  9838  supsrlem  10134  nzadd  11627  fnn0ind  11678  uztrn2  11906  nnwo  11956  irradd  12015  qbtwnxr  12236  xltnegi  12252  xaddnemnf  12272  xaddnepnf  12273  xaddcom  12276  xnegdi  12283  elioore  12410  uzsubsubfz1  12571  fzo1fzo0n0  12727  elfzonelfzo  12778  modsumfzodifsn  12951  leexp2  13122  faclbnd  13281  faclbnd3  13283  fi1uzind  13481  brfi1uzind  13482  opfi1uzind  13485  swrdccat3b  13705  dvdslelem  15240  divalglem1  15325  dvdsprime  15607  pcgcd  15789  cntri  17970  efgsrel  18354  xrsdsreclb  20008  znf1o  20115  restuni  21187  stoig  21188  restperf  21209  resstps  21212  pnfnei  21245  mnfnei  21246  cnnei  21307  cmpsublem  21423  comppfsc  21556  tx1stc  21674  xkopt  21679  isfcls  22033  tgioo  22819  opnreen  22854  iscmet3  23310  dyaddisj  23584  limcmpt  23867  degltlem1  24052  ulmdvlem3  24376  lgsdi  25280  cusgrres  26579  crctcshwlkn0lem4  26941  crctcshwlkn0lem5  26942  wwlksnred  27036  clwlksfclwwlkOLD  27243  eupth2lem3lem4  27411  grpoidinvlem3  27700  ipasslem3  28028  spanuni  28743  5oalem3  28855  5oalem5  28857  mdslmd1lem2  29525  mptctf  29835  xaddeq0  29858  ordtconnlem1  30310  esumcvg  30488  ldgenpisyslem1  30566  measres  30625  measdivcstOLD  30627  measdivcst  30628  probun  30821  elmpps  31808  dfon2lem9  32032  noreson  32150  funpartfun  32387  cgrxfr  32499  segcon2  32549  brsegle2  32553  seglecgr12im  32554  segletr  32558  nn0prpw  32655  bj-seex  33250  lindsenlbs  33737  matunitlindflem2  33739  ptrecube  33742  poimirlem28  33770  ftc1anclem5  33821  ftc1anc  33825  exlimddvfi  34259  prtlem11  34674  mzpclall  37816  4an31  39229  cnrefiisplem  40573  iundjiun  41194  funbrafvb  41756  funopafvb  41757  afvco2  41776  sprsymrelfolem2  42271
  Copyright terms: Public domain W3C validator