Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eqbr Unicode version

Theorem syl6eqbr 4489
 Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
Hypotheses
Ref Expression
syl6eqbr.1
syl6eqbr.2
Assertion
Ref Expression
syl6eqbr

Proof of Theorem syl6eqbr
StepHypRef Expression
1 syl6eqbr.2 . 2
2 syl6eqbr.1 . . 3
32breq1d 4462 . 2
41, 3mpbiri 233 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452 This theorem is referenced by:  syl6eqbrr  4490  domunsn  7687  mapdom1  7702  mapdom2  7708  pm54.43  8402  cdadom1  8587  infmap2  8619  inar1  9174  gruina  9217  xltnegi  11444  leexp1a  12224  discr  12303  facwordi  12367  faclbnd3  12370  hashsnlei  12478  hashgt12el  12481  cnpart  13073  geomulcvg  13685  dvds1  14034  ramz2  14542  ramz  14543  gex1  16611  sylow2a  16639  en1top  19486  en2top  19487  hmph0  20296  ptcmplem2  20553  dscmet  21093  dscopn  21094  xrge0tsms2  21340  htpycc  21480  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  vitalilem5  22021  dvef  22381  dveq0  22401  dv11cn  22402  deg1lt0  22491  ply1rem  22564  fta1g  22568  plyremlem  22700  aalioulem3  22730  pige3  22910  relogrn  22949  logneg  22972  cxpaddlelem  23125  mule1  23422  ppiub  23479  dchrabs2  23537  bposlem1  23559  lgseisen  23628  lgsquadlem2  23630  rpvmasumlem  23672  qabvle  23810  ostth3  23823  colinearalg  24213  eengstr  24283  konigsberg  24987  nmosetn0  25680  nmoo0  25706  siii  25768  bcsiALT  26096  branmfn  27024  ballotlemrc  28469  subfacval3  28633  sconpi1  28684  fz0n  29110  itg2addnclem  30066  ftc1anc  30098  radcnvrat  31195  stoweidlem18  31800  stoweidlem55  31837  fourierdlem62  31951  fourierswlem  32013  exple2lt6  32957 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
 Copyright terms: Public domain W3C validator