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  2839  pm13.181  3096  rmob  3871  sspsstr  4079  disjne  4400  rexopabb  5406  seex  5511  xpcan2  6027  tron  6207  fssres  6537  funbrfvb  6713  funopfvb  6714  fvco  6752  fvimacnvi  6814  ffvresb  6880  funressn  6913  funresdfunsn  6943  fvtp2  6950  fvtp2g  6953  fnex  6971  funex  6973  ordsucss  7522  ordsucelsuc  7526  1st2nd  7727  1stconst  7784  2ndconst  7785  frxp  7809  imacosupp  7863  dftpos4  7900  tz7.48lem  8066  nnmsucr  8240  nnmcan  8249  xpmapenlem  8672  php  8689  php4  8692  isfinite2  8764  fundmfibi  8791  fiinfcl  8953  wofib  8997  r1limg  9188  r1pwcl  9264  cardmin2  9415  zornn0g  9915  mptct  9948  intgru  10224  supsrlem  10521  nzadd  12018  fnn0ind  12069  uztrn2  12250  nnwo  12301  irradd  12360  qbtwnxr  12581  xltnegi  12597  xaddnemnf  12617  xaddnepnf  12618  xaddcom  12621  xnegdi  12629  elioore  12756  uzsubsubfz1  12918  fzo1fzo0n0  13076  elfzonelfzo  13127  modsumfzodifsn  13300  leexp2  13523  faclbnd  13638  faclbnd3  13640  fi1uzind  13843  brfi1uzind  13844  opfi1uzind  13847  swrdccat3b  14090  dvdslelem  15647  divalglem1  15733  dvdsprime  16019  pcgcd  16202  cntri  18399  efgsrel  18789  xrsdsreclb  20520  znf1o  20626  restuni  21698  stoig  21699  restperf  21720  resstps  21723  pnfnei  21756  mnfnei  21757  cnnei  21818  cmpsublem  21935  comppfsc  22068  tx1stc  22186  xkopt  22191  isfcls  22545  tgioo  23331  opnreen  23366  iscmet3  23823  dyaddisj  24124  limcmpt  24408  degltlem1  24593  ulmdvlem3  24917  lgsdi  25837  cusgrres  27157  crctcshwlkn0lem4  27518  crctcshwlkn0lem5  27519  wwlksnred  27597  eupth2lem3lem4  27937  grpoidinvlem3  28210  ipasslem3  28537  spanuni  29248  5oalem3  29360  5oalem5  29362  mdslmd1lem2  30030  mptctf  30379  xaddeq0  30403  xnn0gt0  30420  ordtconnlem1  31066  esumcvg  31244  ldgenpisyslem1  31321  measres  31380  measdivcst  31382  measdivcstALTV  31383  probun  31576  elmpps  32717  dfon2lem9  32933  noreson  33064  funpartfun  33301  cgrxfr  33413  segcon2  33463  brsegle2  33467  seglecgr12im  33468  segletr  33472  nn0prpw  33568  bj-seex  34138  fvineqsneu  34574  lindsenlbs  34768  matunitlindflem2  34770  ptrecube  34773  poimirlem28  34801  ftc1anclem5  34852  ftc1anc  34856  exlimddvfi  35281  mzpclall  39202  4an31  40709  cnrefiisplem  41986  iundjiun  42619  funbrafvb  43232  funopafvb  43233  afvco2  43252  dfatbrafv2b  43321  funbrafv22b  43326  funopafv2b  43327  sprsymrelfolem2  43532  line2xlem  44668  itsclc0xyqsol  44683  setrec2lem2  44725
  Copyright terms: Public domain W3C validator