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

Theorem sylan2br 491
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 216 . 2 (𝜑𝜒)
3 sylan2br.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 489 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  syl2anbr  495  imainss  5452  funeu2  5814  imadif  5872  fnop  5893  ssimaex  6157  tfindsg2  6930  nn0suc  6959  xpexr2  6977  extmptsuppeq  7183  suppss  7189  suppss2  7193  wfr3g  7277  smores3  7314  tfr3ALT  7362  tz7.48-2  7401  swoso  7639  isinf  8035  frfi  8067  dffi3  8197  marypha1lem  8199  ordtypelem7  8289  cnfcom2lem  8458  r1pw  8568  rankxplim3  8604  dfac5  8811  cofsmo  8951  axcclem  9139  zorn2lem7  9184  wloglei  10411  divval  10538  uzind3  11305  xrltnsym  11807  xaddf  11890  xrsupsslem  11967  xrinfmsslem  11968  0fz1  12189  hashunsng  12996  hashgt0elexb  13005  sumss  14250  fsumss  14251  fsumcvg3  14255  abscvgcvg  14340  isumshft  14358  geoisum1  14397  geoisum1c  14398  mertenslem2  14404  zprod  14454  prodss  14464  fprodss  14465  rpnnen2lem5  14734  gcdcllem3  15009  lcmgcd  15106  lcmdvds  15107  lcmfval  15120  lcmfcl  15127  dvdslcmf  15130  eulerthlem2  15273  ramcl2lem  15499  imasvscafn  15968  mreexexlem4d  16078  cycsubgcl  17391  galactghm  17594  odlem2  17729  gexlem2  17768  mulgmhm  18004  mulgghm  18005  gsumval3  18079  gsumpt  18132  dprdfeq0  18192  srglmhm  18306  srgrmhm  18307  ringlghm  18375  ringrghm  18376  lssssr  18722  lbsind  18849  mplmonmul  19233  mplcoe1  19234  mplcoe5  19237  cnsubrg  19573  matplusgcell  20005  elcls  20634  neips  20674  opnnei  20681  ordtbaslem  20749  ptclsg  21175  qtopeu  21276  xmetpsmet  21910  comet  22075  metrest  22086  pcorevlem  22581  dyadmbl  23118  mbfeqalem  23159  i1fadd  23212  itg1addlem2  23214  itg2uba  23260  itgss  23328  dvcnp  23432  quotval  23795  vieta1lem2  23814  aalioulem3  23837  ulmdvlem3  23904  dvradcnv  23923  abelthlem6  23938  abelthlem9  23942  abelth  23943  logtayllem  24149  logtayl  24150  cxpcl  24164  recxpcl  24165  cxpcn3lem  24232  leibpi  24413  musum  24661  dchrelbas3  24707  sumdchr2  24739  lgscllem  24773  lgsdir2  24799  dchrvmasumiflem2  24935  rpvmasum2  24945  padicabv  25063  padicabvf  25064  padicabvcxp  25065  nmooval  26795  hiidge0  27132  hommval  27772  hfmmval  27775  nmcfnlbi  28088  mdslmd1i  28365  mdslmd3i  28368  sumdmdlem2  28455  foresf1o  28520  disjdifprg  28563  cnvoprab  28679  xdivval  28751  esumfsupre  29253  dya2iocnei  29464  eulerpartlemgc  29544  eulerpartlemb  29550  eulerpartlemgh  29560  ballotlemfc0  29674  ballotlemfcc  29675  subfacp1lem5  30213  subfacp1lem6  30214  cvmliftlem10  30323  elmrsubrn  30464  colinearperm1  31132  colinearperm5  31136  endofsegid  31155  segcon2  31175  seglecgr12im  31180  segletr  31184  colinbtwnle  31188  broutsideof2  31192  btwnoutside  31195  outsideoftr  31199  outsidele  31202  opnbnd  31283  matunitlindf  32360  poimirlem11  32373  poimirlem12  32374  poimirlem16  32378  poimirlem19  32381  poimirlem26  32388  heibor1lem  32561  heiborlem3  32565  heiborlem10  32572  ablo4pnp  32632  crngm4  32755  lkrpssN  33251  pclvalN  33977  polvalN  33992  lclkrlem2x  35620  hgmaprnlem5N  35993  sdrgacs  36573  cntzsdrg  36574  dvgrat  37316  radcnvrat  37318  cncfiooicclem1  38562  fourierdlem101  38883  etransclem24  38934  ioorrnopn  38984  11wlkdlem4  41288
  Copyright terms: Public domain W3C validator