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

Theorem eqbrtrdi 5145
Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrdi.1 (𝜑𝐴 = 𝐵)
eqbrtrdi.2 𝐵𝑅𝐶
Assertion
Ref Expression
eqbrtrdi (𝜑𝐴𝑅𝐶)

Proof of Theorem eqbrtrdi
StepHypRef Expression
1 eqbrtrdi.2 . 2 𝐵𝑅𝐶
2 eqbrtrdi.1 . . 3 (𝜑𝐴 = 𝐵)
32breq1d 5116 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbiri 258 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  eqbrtrrdi  5146  domunsn  9072  mapdom1  9087  mapdom2  9093  pm54.43  9938  infmap2  10155  inar1  10712  gruina  10755  nn0ledivnn  13029  xltnegi  13136  leexp1a  14081  discr  14144  facwordi  14190  faclbnd3  14193  hashgt12el  14323  hashle2pr  14377  cnpart  15126  geomulcvg  15762  dvds1  16202  ramz2  16897  ramz  16898  gex1  19374  sylow2a  19402  en1top  22337  en2top  22338  hmph0  23149  ptcmplem2  23407  dscmet  23931  dscopn  23932  xrge0tsms2  24201  htpycc  24346  pcohtpylem  24385  pcopt  24388  pcopt2  24389  pcoass  24390  pcorevlem  24392  vitalilem5  24979  dvef  25347  dveq0  25367  dv11cn  25368  deg1lt0  25459  ply1rem  25531  fta1g  25535  plyremlem  25667  aalioulem3  25697  pige3ALT  25879  relogrn  25920  logneg  25946  cxpaddlelem  26107  mule1  26500  ppiub  26555  dchrabs2  26613  bposlem1  26635  zabsle1  26647  lgseisen  26730  lgsquadlem2  26732  rpvmasumlem  26838  qabvle  26976  ostth3  26989  colinearalg  27862  eengstr  27932  clwwlknon1le1  29048  eucrct2eupth  29192  nmosetn0  29710  nmoo0  29736  siii  29798  bcsiALT  30124  branmfn  31050  esumrnmpt2  32670  ballotlemrc  33133  pthhashvtx  33724  subfacval3  33786  sconnpi1  33836  fz0n  34306  poimirlem31  36112  itg2addnclem  36132  ftc1anc  36162  safesnsupfidom1o  41696  radcnvrat  42601  infxr  43608  stoweidlem18  44266  stoweidlem55  44303  fourierdlem62  44416  fourierswlem  44478  exple2lt6  46447  fvconstdomi  46933  f1omoALT  46935  indthincALT  47080
  Copyright terms: Public domain W3C validator