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

Theorem syl6eqbr 4662
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 4633 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbiri 248 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480   class class class wbr 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624
This theorem is referenced by:  syl6eqbrr  4663  domunsn  8070  mapdom1  8085  mapdom2  8091  pm54.43  8786  cdadom1  8968  infmap2  9000  inar1  9557  gruina  9600  nn0ledivnn  11901  xltnegi  12006  leexp1a  12875  discr  12957  facwordi  13032  faclbnd3  13035  hashgt12el  13166  hashle2pr  13213  cnpart  13930  geomulcvg  14551  dvds1  14984  ramz2  15671  ramz  15672  gex1  17946  sylow2a  17974  en1top  20728  en2top  20729  hmph0  21538  ptcmplem2  21797  dscmet  22317  dscopn  22318  xrge0tsms2  22578  htpycc  22719  pcohtpylem  22759  pcopt  22762  pcopt2  22763  pcoass  22764  pcorevlem  22766  vitalilem5  23321  dvef  23681  dveq0  23701  dv11cn  23702  deg1lt0  23789  ply1rem  23861  fta1g  23865  plyremlem  23997  aalioulem3  24027  pige3  24207  relogrn  24246  logneg  24272  cxpaddlelem  24426  mule1  24808  ppiub  24863  dchrabs2  24921  bposlem1  24943  zabsle1  24955  lgseisen  25038  lgsquadlem2  25040  rpvmasumlem  25110  qabvle  25248  ostth3  25261  colinearalg  25724  eengstr  25794  eucrct2eupth  27005  nmosetn0  27508  nmoo0  27534  siii  27596  bcsiALT  27924  branmfn  28852  esumrnmpt2  29953  ballotlemrc  30415  subfacval3  30932  sconnpi1  30982  fz0n  31377  poimirlem31  33111  itg2addnclem  33132  ftc1anc  33164  radcnvrat  38034  infxr  39082  stoweidlem18  39572  stoweidlem55  39609  fourierdlem62  39722  fourierswlem  39784  exple2lt6  41463
  Copyright terms: Public domain W3C validator