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

Theorem sylan2br 494
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 492 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  498  pm2.61danel  3049  imainss  5706  funeu2  6075  imadif  6134  fnop  6155  ssimaex  6426  tfindsg2  7227  nn0suc  7256  xpexr2  7273  extmptsuppeq  7488  suppss  7495  suppss2  7499  wfr3g  7583  smores3  7620  tfr3ALT  7668  tz7.48-2  7707  swoso  7946  isinf  8340  frfi  8372  dffi3  8504  marypha1lem  8506  ordtypelem7  8596  cnfcom2lem  8773  r1pw  8883  rankxplim3  8919  dfac5  9161  cofsmo  9303  axcclem  9491  zorn2lem7  9536  wloglei  10772  divval  10899  uzind3  11683  xrltnsym  12183  xaddf  12268  xrsupsslem  12350  xrinfmsslem  12351  0fz1  12574  hashunsng  13393  hashgt0elexb  13402  sumss  14674  fsumss  14675  fsumcvg3  14679  abscvgcvg  14770  isumshft  14790  geoisum1  14829  geoisum1c  14830  mertenslem2  14836  zprod  14886  prodss  14896  fprodss  14897  rpnnen2lem5  15166  gcdcllem3  15445  lcmgcd  15542  lcmdvds  15543  lcmfval  15556  lcmfcl  15563  dvdslcmf  15566  isprm2lem  15616  eulerthlem2  15709  ramcl2lem  15935  imasvscafn  16419  mreexexlem4d  16529  cycsubgcl  17841  galactghm  18043  odlem2  18178  gexlem2  18217  mulgmhm  18453  mulgghm  18454  gsumval3  18528  gsumpt  18581  dprdfeq0  18641  srglmhm  18755  srgrmhm  18756  ringlghm  18824  ringrghm  18825  lssssr  19175  lbsind  19302  mplmonmul  19686  mplcoe1  19687  mplcoe5  19690  cnsubrg  20028  matplusgcell  20461  elcls  21099  neips  21139  opnnei  21146  ordtbaslem  21214  ptclsg  21640  qtopeu  21741  xmetpsmet  22374  comet  22539  metrest  22550  pcorevlem  23046  dyadmbl  23588  mbfeqalem  23628  i1fadd  23681  itg1addlem2  23683  itg2uba  23729  itgss  23797  dvcnp  23901  quotval  24266  vieta1lem2  24285  aalioulem3  24308  ulmdvlem3  24375  dvradcnv  24394  abelthlem6  24409  abelthlem9  24413  abelth  24414  logtayllem  24625  logtayl  24626  cxpcl  24640  recxpcl  24641  cxpcn3lem  24708  leibpi  24889  musum  25137  dchrelbas3  25183  sumdchr2  25215  lgscllem  25249  lgsdir2  25275  dchrvmasumiflem2  25411  rpvmasum2  25421  padicabv  25539  padicabvf  25540  padicabvcxp  25541  1wlkdlem4  27313  nmooval  27948  hiidge0  28285  hommval  28925  hfmmval  28928  nmcfnlbi  29241  mdslmd1i  29518  mdslmd3i  29521  sumdmdlem2  29608  foresf1o  29671  disjdifprg  29716  cnvoprabOLD  29828  xdivval  29957  esumfsupre  30463  dya2iocnei  30674  eulerpartlemgc  30754  eulerpartlemb  30760  eulerpartlemgh  30770  ballotlemfc0  30884  ballotlemfcc  30885  subfacp1lem5  31494  subfacp1lem6  31495  cvmliftlem10  31604  elmrsubrn  31745  colinearperm1  32496  colinearperm5  32500  endofsegid  32519  segcon2  32539  seglecgr12im  32544  segletr  32548  colinbtwnle  32552  broutsideof2  32556  btwnoutside  32559  outsideoftr  32563  outsidele  32566  opnbnd  32647  matunitlindf  33738  poimirlem11  33751  poimirlem12  33752  poimirlem16  33756  poimirlem19  33759  poimirlem26  33766  heibor1lem  33939  heiborlem3  33943  heiborlem10  33950  ablo4pnp  34010  crngm4  34133  lkrpssN  34971  pclvalN  35697  polvalN  35712  lclkrlem2x  37339  hgmaprnlem5N  37712  sdrgacs  38291  cntzsdrg  38292  dvgrat  39031  radcnvrat  39033  cncfiooicclem1  40627  fourierdlem101  40945  etransclem24  40996  ioorrnopn  41046
  Copyright terms: Public domain W3C validator