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

Theorem sylan2br 492
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 218 . 2 (𝜑𝜒)
3 sylan2br.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 490 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  syl2anbr  496  pm2.61danel  2940  imainss  5583  funeu2  5952  imadif  6011  fnop  6032  ssimaex  6302  tfindsg2  7103  nn0suc  7132  xpexr2  7149  extmptsuppeq  7364  suppss  7370  suppss2  7374  wfr3g  7458  smores3  7495  tfr3ALT  7543  tz7.48-2  7582  swoso  7820  isinf  8214  frfi  8246  dffi3  8378  marypha1lem  8380  ordtypelem7  8470  cnfcom2lem  8636  r1pw  8746  rankxplim3  8782  dfac5  8989  cofsmo  9129  axcclem  9317  zorn2lem7  9362  wloglei  10598  divval  10725  uzind3  11509  xrltnsym  12008  xaddf  12093  xrsupsslem  12175  xrinfmsslem  12176  0fz1  12399  hashunsng  13219  hashgt0elexb  13228  sumss  14499  fsumss  14500  fsumcvg3  14504  abscvgcvg  14595  isumshft  14615  geoisum1  14654  geoisum1c  14655  mertenslem2  14661  zprod  14711  prodss  14721  fprodss  14722  rpnnen2lem5  14991  gcdcllem3  15270  lcmgcd  15367  lcmdvds  15368  lcmfval  15381  lcmfcl  15388  dvdslcmf  15391  isprm2lem  15441  eulerthlem2  15534  ramcl2lem  15760  imasvscafn  16244  mreexexlem4d  16354  cycsubgcl  17667  galactghm  17869  odlem2  18004  gexlem2  18043  mulgmhm  18279  mulgghm  18280  gsumval3  18354  gsumpt  18407  dprdfeq0  18467  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  lssssr  19001  lbsind  19128  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  cnsubrg  19854  matplusgcell  20287  elcls  20925  neips  20965  opnnei  20972  ordtbaslem  21040  ptclsg  21466  qtopeu  21567  xmetpsmet  22200  comet  22365  metrest  22376  pcorevlem  22872  dyadmbl  23414  mbfeqalem  23454  i1fadd  23507  itg1addlem2  23509  itg2uba  23555  itgss  23623  dvcnp  23727  quotval  24092  vieta1lem2  24111  aalioulem3  24134  ulmdvlem3  24201  dvradcnv  24220  abelthlem6  24235  abelthlem9  24239  abelth  24240  logtayllem  24450  logtayl  24451  cxpcl  24465  recxpcl  24466  cxpcn3lem  24533  leibpi  24714  musum  24962  dchrelbas3  25008  sumdchr2  25040  lgscllem  25074  lgsdir2  25100  dchrvmasumiflem2  25236  rpvmasum2  25246  padicabv  25364  padicabvf  25365  padicabvcxp  25366  1wlkdlem4  27118  nmooval  27746  hiidge0  28083  hommval  28723  hfmmval  28726  nmcfnlbi  29039  mdslmd1i  29316  mdslmd3i  29319  sumdmdlem2  29406  foresf1o  29469  disjdifprg  29514  cnvoprabOLD  29626  xdivval  29755  esumfsupre  30261  dya2iocnei  30472  eulerpartlemgc  30552  eulerpartlemb  30558  eulerpartlemgh  30568  ballotlemfc0  30682  ballotlemfcc  30683  subfacp1lem5  31292  subfacp1lem6  31293  cvmliftlem10  31402  elmrsubrn  31543  colinearperm1  32294  colinearperm5  32298  endofsegid  32317  segcon2  32337  seglecgr12im  32342  segletr  32346  colinbtwnle  32350  broutsideof2  32354  btwnoutside  32357  outsideoftr  32361  outsidele  32364  opnbnd  32445  matunitlindf  33537  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem19  33558  poimirlem26  33565  heibor1lem  33738  heiborlem3  33742  heiborlem10  33749  ablo4pnp  33809  crngm4  33932  lkrpssN  34768  pclvalN  35494  polvalN  35509  lclkrlem2x  37136  hgmaprnlem5N  37509  sdrgacs  38088  cntzsdrg  38089  dvgrat  38828  radcnvrat  38830  cncfiooicclem1  40424  fourierdlem101  40742  etransclem24  40793  ioorrnopn  40843
  Copyright terms: Public domain W3C validator