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  3134  imainss  6004  funeu2  6374  imadif  6431  fnop  6453  ssimaex  6741  tfindsg2  7565  nn0suc  7595  xpexr2  7613  extmptsuppeq  7843  suppss  7849  suppss2  7853  wfr3g  7942  smores3  7979  tfr3ALT  8027  tz7.48-2  8067  swoso  8311  isinf  8719  frfi  8751  dffi3  8883  marypha1lem  8885  ordtypelem7  8976  cnfcom2lem  9152  r1pw  9262  rankxplim3  9298  dfac5  9542  cofsmo  9679  axcclem  9867  zorn2lem7  9912  wloglei  11160  divval  11288  uzind3  12064  xrltnsym  12518  xaddf  12605  xrsupsslem  12688  xrinfmsslem  12689  0fz1  12915  hashunsng  13741  hashunsngx  13742  hashgt0elexb  13751  sumss  15069  fsumss  15070  fsumcvg3  15074  abscvgcvg  15162  isumshft  15182  geoisum1  15223  geoisum1c  15224  mertenslem2  15229  zprod  15279  prodss  15289  fprodss  15290  rpnnen2lem5  15559  gcdcllem3  15838  lcmgcd  15939  lcmdvds  15940  lcmfval  15953  lcmfcl  15960  dvdslcmf  15963  isprm2lem  16013  eulerthlem2  16107  ramcl2lem  16333  imasvscafn  16798  mreexexlem4d  16906  cycsubgcl  18287  galactghm  18461  odlem2  18596  gexlem2  18636  mulgmhm  18877  mulgghm  18878  gsumval3  18956  gsumpt  19011  dprdfeq0  19073  srglmhm  19214  srgrmhm  19215  ringlghm  19283  ringrghm  19284  sdrgacs  19509  cntzsdrg  19510  lssssr  19654  lbsind  19781  mplmonmul  20173  mplcoe1  20174  mplcoe5  20177  cnsubrg  20533  matplusgcell  20970  elcls  21609  neips  21649  opnnei  21656  ordtbaslem  21724  ptclsg  22151  qtopeu  22252  xmetpsmet  22885  comet  23050  metrest  23061  pcorevlem  23557  dyadmbl  24128  mbfeqalem1  24169  i1fadd  24223  itg1addlem2  24225  itg2uba  24271  itgss  24339  dvcnp  24443  quotval  24808  vieta1lem2  24827  aalioulem3  24850  ulmdvlem3  24917  dvradcnv  24936  abelthlem6  24951  abelthlem9  24955  abelth  24956  logtayllem  25169  logtayl  25170  cxpcl  25184  recxpcl  25185  cxpcn3lem  25255  leibpi  25447  musum  25695  dchrelbas3  25741  sumdchr2  25773  lgscllem  25807  lgsdir2  25833  dchrvmasumiflem2  26005  rpvmasum2  26015  padicabv  26133  padicabvf  26134  padicabvcxp  26135  1wlkdlem4  27846  nmooval  28467  hiidge0  28802  hommval  29440  hfmmval  29443  nmcfnlbi  29756  mdslmd1i  30033  mdslmd3i  30036  sumdmdlem2  30123  foresf1o  30192  disjdifprg  30253  cnvoprabOLD  30382  xdivval  30522  esumfsupre  31229  dya2iocnei  31439  eulerpartlemgc  31519  eulerpartlemb  31525  eulerpartlemgh  31535  ballotlemfc0  31649  ballotlemfcc  31650  subfacp1lem5  32328  subfacp1lem6  32329  cvmliftlem10  32438  elmrsubrn  32664  frrlem14  33033  colinearperm1  33420  colinearperm5  33424  endofsegid  33443  segcon2  33463  seglecgr12im  33468  segletr  33472  colinbtwnle  33476  broutsideof2  33480  btwnoutside  33483  outsideoftr  33487  outsidele  33490  opnbnd  33570  ctbssinf  34569  matunitlindf  34771  poimirlem11  34784  poimirlem12  34785  poimirlem16  34789  poimirlem19  34792  poimirlem26  34799  heibor1lem  34968  heiborlem3  34972  heiborlem10  34979  ablo4pnp  35039  crngm4  35162  lkrpssN  36179  pclvalN  36906  polvalN  36921  lclkrlem2x  38546  hgmaprnlem5N  38916  dvgrat  40521  radcnvrat  40523  cncfiooicclem1  42052  fourierdlem101  42369  etransclem24  42420  ioorrnopn  42467
  Copyright terms: Public domain W3C validator