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

Theorem syl6eqbr 4844
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 4815 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbiri 248 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632   class class class wbr 4805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806
This theorem is referenced by:  syl6eqbrr  4845  domunsn  8278  mapdom1  8293  mapdom2  8299  pm54.43  9037  cdadom1  9221  infmap2  9253  inar1  9810  gruina  9853  nn0ledivnn  12155  xltnegi  12261  leexp1a  13134  discr  13216  facwordi  13291  faclbnd3  13294  hashgt12el  13423  hashle2pr  13472  cnpart  14200  geomulcvg  14827  dvds1  15264  ramz2  15951  ramz  15952  gex1  18227  sylow2a  18255  en1top  21011  en2top  21012  hmph0  21821  ptcmplem2  22079  dscmet  22599  dscopn  22600  xrge0tsms2  22860  htpycc  23001  pcohtpylem  23040  pcopt  23043  pcopt2  23044  pcoass  23045  pcorevlem  23047  vitalilem5  23601  dvef  23963  dveq0  23983  dv11cn  23984  deg1lt0  24071  ply1rem  24143  fta1g  24147  plyremlem  24279  aalioulem3  24309  pige3  24490  relogrn  24529  logneg  24555  cxpaddlelem  24713  mule1  25095  ppiub  25150  dchrabs2  25208  bposlem1  25230  zabsle1  25242  lgseisen  25325  lgsquadlem2  25327  rpvmasumlem  25397  qabvle  25535  ostth3  25548  colinearalg  26011  eengstr  26081  clwwlknon1le1  27271  eucrct2eupth  27419  nmosetn0  27951  nmoo0  27977  siii  28039  bcsiALT  28367  branmfn  29295  esumrnmpt2  30461  ballotlemrc  30923  subfacval3  31500  sconnpi1  31550  fz0n  31945  poimirlem31  33772  itg2addnclem  33793  ftc1anc  33825  radcnvrat  39034  infxr  40100  stoweidlem18  40757  stoweidlem55  40794  fourierdlem62  40907  fourierswlem  40969  exple2lt6  42674
  Copyright terms: Public domain W3C validator