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

Theorem sylanb 572
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 207 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 571 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  syl2anb  587  anabsan  647  eqtr2  2833  pm13.181  3067  rmob  3731  sspsstr  3917  disjne  4226  seex  5281  xpcan2  5789  tron  5966  fssres  6288  funbrfvb  6461  funopfvb  6462  fvco  6498  fvimacnvi  6556  ffvresb  6619  funressn  6653  funresdfunsn  6683  fvtp2  6689  fvtp2g  6692  fnex  6709  funex  6710  ordsucss  7251  ordsucelsuc  7255  1st2nd  7449  frxp  7524  dftpos4  7609  tz7.48lem  7775  nnmsucr  7945  nnmcan  7954  xpmapenlem  8369  php  8386  php4  8389  isfinite2  8460  fundmfibi  8487  fiinfcl  8649  wofib  8692  r1limg  8884  r1pwcl  8960  cardmin2  9110  zornn0g  9615  mptct  9648  intgru  9924  supsrlem  10220  nzadd  11694  fnn0ind  11745  uztrn2  11925  nnwo  11975  irradd  12034  qbtwnxr  12252  xltnegi  12268  xaddnemnf  12288  xaddnepnf  12289  xaddcom  12292  xnegdi  12299  elioore  12426  uzsubsubfz1  12590  fzo1fzo0n0  12746  elfzonelfzo  12797  modsumfzodifsn  12970  leexp2  13141  faclbnd  13300  faclbnd3  13302  fi1uzind  13499  brfi1uzind  13500  opfi1uzind  13503  swrdccat3b  13723  dvdslelem  15257  divalglem1  15340  dvdsprime  15621  pcgcd  15802  cntri  17967  efgsrel  18351  xrsdsreclb  20004  znf1o  20110  restuni  21184  stoig  21185  restperf  21206  resstps  21209  pnfnei  21242  mnfnei  21243  cnnei  21304  cmpsublem  21420  comppfsc  21553  tx1stc  21671  xkopt  21676  isfcls  22030  tgioo  22816  opnreen  22851  iscmet3  23308  dyaddisj  23583  limcmpt  23867  degltlem1  24052  ulmdvlem3  24376  lgsdi  25279  cusgrres  26578  crctcshwlkn0lem4  26940  crctcshwlkn0lem5  26941  wwlksnred  27035  clwlksfclwwlkOLD  27242  eupth2lem3lem4  27410  grpoidinvlem3  27695  ipasslem3  28022  spanuni  28737  5oalem3  28849  5oalem5  28851  mdslmd1lem2  29519  mptctf  29828  xaddeq0  29851  ordtconnlem1  30301  esumcvg  30479  ldgenpisyslem1  30557  measres  30616  measdivcstOLD  30618  measdivcst  30619  probun  30812  elmpps  31798  dfon2lem9  32021  noreson  32139  funpartfun  32376  cgrxfr  32488  segcon2  32538  brsegle2  32542  seglecgr12im  32543  segletr  32547  nn0prpw  32644  bj-seex  33231  lindsenlbs  33719  matunitlindflem2  33721  ptrecube  33724  poimirlem28  33752  ftc1anclem5  33803  ftc1anc  33807  exlimddvfi  34239  prtlem11  34647  mzpclall  37793  4an31  39203  cnrefiisplem  40536  iundjiun  41157  funbrafvb  41746  funopafvb  41747  afvco2  41766  dfatbrafv2b  41835  funbrafv22b  41840  funopafv2b  41841  sprsymrelfolem2  42312
  Copyright terms: Public domain W3C validator