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

Theorem sylan2br 594
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 229 . 2 (𝜑𝜒)
3 sylan2br.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 592 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:  syl2anbr  598  pm2.61danel  3137  imainss  6005  funeu2  6375  imadif  6432  fnop  6454  ssimaex  6742  tfindsg2  7564  nn0suc  7594  xpexr2  7612  extmptsuppeq  7845  suppss  7851  suppss2  7855  wfr3g  7944  smores3  7981  tfr3ALT  8029  tz7.48-2  8069  swoso  8312  isinf  8720  frfi  8752  dffi3  8884  marypha1lem  8886  ordtypelem7  8977  cnfcom2lem  9153  r1pw  9263  rankxplim3  9299  dfac5  9543  cofsmo  9680  axcclem  9868  zorn2lem7  9913  wloglei  11161  divval  11289  uzind3  12065  xrltnsym  12520  xaddf  12607  xrsupsslem  12690  xrinfmsslem  12691  0fz1  12917  hashunsng  13743  hashunsngx  13744  hashgt0elexb  13753  sumss  15071  fsumss  15072  fsumcvg3  15076  abscvgcvg  15164  isumshft  15184  geoisum1  15225  geoisum1c  15226  mertenslem2  15231  zprod  15281  prodss  15291  fprodss  15292  rpnnen2lem5  15561  gcdcllem3  15840  lcmgcd  15941  lcmdvds  15942  lcmfval  15955  lcmfcl  15962  dvdslcmf  15965  isprm2lem  16015  eulerthlem2  16109  ramcl2lem  16335  imasvscafn  16800  mreexexlem4d  16908  cycsubgcl  18289  galactghm  18463  odlem2  18598  gexlem2  18638  mulgmhm  18879  mulgghm  18880  gsumval3  18958  gsumpt  19013  dprdfeq0  19075  srglmhm  19216  srgrmhm  19217  ringlghm  19285  ringrghm  19286  sdrgacs  19511  cntzsdrg  19512  lssssr  19656  lbsind  19783  mplmonmul  20175  mplcoe1  20176  mplcoe5  20179  cnsubrg  20535  matplusgcell  20972  elcls  21611  neips  21651  opnnei  21658  ordtbaslem  21726  ptclsg  22153  qtopeu  22254  xmetpsmet  22887  comet  23052  metrest  23063  pcorevlem  23559  dyadmbl  24130  mbfeqalem1  24171  i1fadd  24225  itg1addlem2  24227  itg2uba  24273  itgss  24341  dvcnp  24445  quotval  24810  vieta1lem2  24829  aalioulem3  24852  ulmdvlem3  24919  dvradcnv  24938  abelthlem6  24953  abelthlem9  24957  abelth  24958  logtayllem  25169  logtayl  25170  cxpcl  25184  recxpcl  25185  cxpcn3lem  25255  leibpi  25448  musum  25696  dchrelbas3  25742  sumdchr2  25774  lgscllem  25808  lgsdir2  25834  dchrvmasumiflem2  26006  rpvmasum2  26016  padicabv  26134  padicabvf  26135  padicabvcxp  26136  1wlkdlem4  27847  nmooval  28468  hiidge0  28803  hommval  29441  hfmmval  29444  nmcfnlbi  29757  mdslmd1i  30034  mdslmd3i  30037  sumdmdlem2  30124  foresf1o  30193  disjdifprg  30254  cnvoprabOLD  30383  xdivval  30523  esumfsupre  31230  dya2iocnei  31440  eulerpartlemgc  31520  eulerpartlemb  31526  eulerpartlemgh  31536  ballotlemfc0  31650  ballotlemfcc  31651  subfacp1lem5  32329  subfacp1lem6  32330  cvmliftlem10  32439  elmrsubrn  32665  frrlem14  33034  colinearperm1  33421  colinearperm5  33425  endofsegid  33444  segcon2  33464  seglecgr12im  33469  segletr  33473  colinbtwnle  33477  broutsideof2  33481  btwnoutside  33484  outsideoftr  33488  outsidele  33491  opnbnd  33571  ctbssinf  34570  matunitlindf  34772  poimirlem11  34785  poimirlem12  34786  poimirlem16  34790  poimirlem19  34793  poimirlem26  34800  heibor1lem  34970  heiborlem3  34974  heiborlem10  34981  ablo4pnp  35041  crngm4  35164  lkrpssN  36181  pclvalN  36908  polvalN  36923  lclkrlem2x  38548  hgmaprnlem5N  38918  dvgrat  40524  radcnvrat  40526  cncfiooicclem1  42056  fourierdlem101  42373  etransclem24  42424  ioorrnopn  42471
  Copyright terms: Public domain W3C validator