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 217 . 2 (𝜑𝜒)
3 sylan2br.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 490 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  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 196  df-an 385
This theorem is referenced by:  syl2anbr  496  imainss  5467  funeu2  5829  imadif  5887  fnop  5908  ssimaex  6173  tfindsg2  6953  nn0suc  6982  xpexr2  7000  extmptsuppeq  7206  suppss  7212  suppss2  7216  wfr3g  7300  smores3  7337  tfr3ALT  7385  tz7.48-2  7424  swoso  7662  isinf  8058  frfi  8090  dffi3  8220  marypha1lem  8222  ordtypelem7  8312  cnfcom2lem  8481  r1pw  8591  rankxplim3  8627  dfac5  8834  cofsmo  8974  axcclem  9162  zorn2lem7  9207  wloglei  10439  divval  10566  uzind3  11347  xrltnsym  11846  xaddf  11929  xrsupsslem  12009  xrinfmsslem  12010  0fz1  12232  hashunsng  13042  hashgt0elexb  13051  sumss  14302  fsumss  14303  fsumcvg3  14307  abscvgcvg  14392  isumshft  14410  geoisum1  14449  geoisum1c  14450  mertenslem2  14456  zprod  14506  prodss  14516  fprodss  14517  rpnnen2lem5  14786  gcdcllem3  15061  lcmgcd  15158  lcmdvds  15159  lcmfval  15172  lcmfcl  15179  dvdslcmf  15182  eulerthlem2  15325  ramcl2lem  15551  imasvscafn  16020  mreexexlem4d  16130  cycsubgcl  17443  galactghm  17646  odlem2  17781  gexlem2  17820  mulgmhm  18056  mulgghm  18057  gsumval3  18131  gsumpt  18184  dprdfeq0  18244  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  lssssr  18774  lbsind  18901  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  cnsubrg  19625  matplusgcell  20058  elcls  20687  neips  20727  opnnei  20734  ordtbaslem  20802  ptclsg  21228  qtopeu  21329  xmetpsmet  21963  comet  22128  metrest  22139  pcorevlem  22634  dyadmbl  23174  mbfeqalem  23215  i1fadd  23268  itg1addlem2  23270  itg2uba  23316  itgss  23384  dvcnp  23488  quotval  23851  vieta1lem2  23870  aalioulem3  23893  ulmdvlem3  23960  dvradcnv  23979  abelthlem6  23994  abelthlem9  23998  abelth  23999  logtayllem  24205  logtayl  24206  cxpcl  24220  recxpcl  24221  cxpcn3lem  24288  leibpi  24469  musum  24717  dchrelbas3  24763  sumdchr2  24795  lgscllem  24829  lgsdir2  24855  dchrvmasumiflem2  24991  rpvmasum2  25001  padicabv  25119  padicabvf  25120  padicabvcxp  25121  nmooval  27002  hiidge0  27339  hommval  27979  hfmmval  27982  nmcfnlbi  28295  mdslmd1i  28572  mdslmd3i  28575  sumdmdlem2  28662  foresf1o  28727  disjdifprg  28770  cnvoprab  28886  xdivval  28958  esumfsupre  29460  dya2iocnei  29671  eulerpartlemgc  29751  eulerpartlemb  29757  eulerpartlemgh  29767  ballotlemfc0  29881  ballotlemfcc  29882  subfacp1lem5  30420  subfacp1lem6  30421  cvmliftlem10  30530  elmrsubrn  30671  colinearperm1  31339  colinearperm5  31343  endofsegid  31362  segcon2  31382  seglecgr12im  31387  segletr  31391  colinbtwnle  31395  broutsideof2  31399  btwnoutside  31402  outsideoftr  31406  outsidele  31409  opnbnd  31490  matunitlindf  32577  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem19  32598  poimirlem26  32605  heibor1lem  32778  heiborlem3  32782  heiborlem10  32789  ablo4pnp  32849  crngm4  32972  lkrpssN  33468  pclvalN  34194  polvalN  34209  lclkrlem2x  35837  hgmaprnlem5N  36210  sdrgacs  36790  cntzsdrg  36791  dvgrat  37533  radcnvrat  37535  cncfiooicclem1  38779  fourierdlem101  39100  etransclem24  39151  ioorrnopn  39201  11wlkdlem4  41307
  Copyright terms: Public domain W3C validator