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

Theorem sylan2br 597
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1 (𝜒𝜑)
sylan2br.2 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylan2br ((𝜓𝜑) → 𝜃)

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3 (𝜒𝜑)
21biimpri 231 . 2 (𝜑𝜒)
3 sylan2br.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 595 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  syl2anbr  601  pm2.61danel  3108  imainss  5982  funeu2  6354  imadif  6412  fnop  6435  ssimaex  6727  tfindsg2  7560  nn0suc  7590  xpexr2  7610  extmptsuppeq  7841  suppss  7847  suppss2  7851  wfr3g  7940  smores3  7977  tfr3ALT  8025  tz7.48-2  8065  swoso  8309  isinf  8719  frfi  8751  dffi3  8883  marypha1lem  8885  ordtypelem7  8976  cnfcom2lem  9152  r1pw  9262  rankxplim3  9298  dfac5  9543  cofsmo  9684  axcclem  9872  zorn2lem7  9917  wloglei  11165  divval  11293  uzind3  12068  xrltnsym  12522  xaddf  12609  xrsupsslem  12692  xrinfmsslem  12693  0fz1  12926  hashunsng  13753  hashunsngx  13754  hashgt0elexb  13763  sumss  15076  fsumss  15077  fsumcvg3  15081  abscvgcvg  15169  isumshft  15189  geoisum1  15230  geoisum1c  15231  mertenslem2  15236  zprod  15286  prodss  15296  fprodss  15297  rpnnen2lem5  15566  gcdcllem3  15843  lcmgcd  15944  lcmdvds  15945  lcmfval  15958  lcmfcl  15965  dvdslcmf  15968  isprm2lem  16018  eulerthlem2  16112  ramcl2lem  16338  imasvscafn  16805  mreexexlem4d  16913  cycsubgcl  18344  galactghm  18527  odlem2  18662  gexlem2  18702  mulgmhm  18944  mulgghm  18945  gsumval3  19023  gsumpt  19078  dprdfeq0  19140  srglmhm  19281  srgrmhm  19282  ringlghm  19353  ringrghm  19354  sdrgacs  19576  cntzsdrg  19577  lssssr  19721  lbsind  19848  cnsubrg  20154  mplmonmul  20707  mplcoe1  20708  mplcoe5  20711  matplusgcell  21041  elcls  21681  neips  21721  opnnei  21728  ordtbaslem  21796  ptclsg  22223  qtopeu  22324  xmetpsmet  22958  comet  23123  metrest  23134  pcorevlem  23634  dyadmbl  24207  mbfeqalem1  24248  i1fadd  24302  itg1addlem2  24304  itg2uba  24350  itgss  24418  dvcnp  24525  quotval  24891  vieta1lem2  24910  aalioulem3  24933  ulmdvlem3  25000  dvradcnv  25019  abelthlem6  25034  abelthlem9  25038  abelth  25039  logtayllem  25253  logtayl  25254  cxpcl  25268  recxpcl  25269  cxpcn3lem  25339  leibpi  25531  musum  25779  dchrelbas3  25825  sumdchr2  25857  lgscllem  25891  lgsdir2  25917  dchrvmasumiflem2  26089  rpvmasum2  26099  padicabv  26217  padicabvf  26218  padicabvcxp  26219  1wlkdlem4  27928  nmooval  28549  hiidge0  28884  hommval  29522  hfmmval  29525  nmcfnlbi  29838  mdslmd1i  30115  mdslmd3i  30118  sumdmdlem2  30205  foresf1o  30276  disjdifprg  30341  cnvoprabOLD  30485  xdivval  30624  esumfsupre  31438  dya2iocnei  31648  eulerpartlemgc  31728  eulerpartlemb  31734  eulerpartlemgh  31744  ballotlemfc0  31858  ballotlemfcc  31859  subfacp1lem5  32539  subfacp1lem6  32540  cvmliftlem10  32649  elmrsubrn  32875  frrlem14  33244  colinearperm1  33631  colinearperm5  33635  endofsegid  33654  segcon2  33674  seglecgr12im  33679  segletr  33683  colinbtwnle  33687  broutsideof2  33691  btwnoutside  33694  outsideoftr  33698  outsidele  33701  opnbnd  33781  ctbssinf  34818  matunitlindf  35048  poimirlem11  35061  poimirlem12  35062  poimirlem16  35066  poimirlem19  35069  poimirlem26  35076  heibor1lem  35240  heiborlem3  35244  heiborlem10  35251  ablo4pnp  35311  crngm4  35434  lkrpssN  36452  pclvalN  37179  polvalN  37194  lclkrlem2x  38819  hgmaprnlem5N  39189  fsuppssindlem1  39444  dvgrat  41003  radcnvrat  41005  cncfiooicclem1  42522  fourierdlem101  42836  etransclem24  42887  ioorrnopn  42934
  Copyright terms: Public domain W3C validator