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

Theorem eqbrtrdi 5092
 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 5063 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbiri 261 1 (𝜑𝐴𝑅𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5053 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-sn 4551  df-pr 4553  df-op 4557  df-br 5054 This theorem is referenced by:  eqbrtrrdi  5093  domunsn  8660  mapdom1  8675  mapdom2  8681  pm54.43  9423  infmap2  9634  inar1  10191  gruina  10234  nn0ledivnn  12497  xltnegi  12604  leexp1a  13542  discr  13604  facwordi  13652  faclbnd3  13655  hashgt12el  13786  hashle2pr  13838  cnpart  14597  geomulcvg  15230  dvds1  15667  ramz2  16356  ramz  16357  gex1  18714  sylow2a  18742  en1top  21587  en2top  21588  hmph0  22398  ptcmplem2  22656  dscmet  23177  dscopn  23178  xrge0tsms2  23438  htpycc  23583  pcohtpylem  23622  pcopt  23625  pcopt2  23626  pcoass  23627  pcorevlem  23629  vitalilem5  24214  dvef  24581  dveq0  24601  dv11cn  24602  deg1lt0  24690  ply1rem  24762  fta1g  24766  plyremlem  24898  aalioulem3  24928  pige3ALT  25110  relogrn  25151  logneg  25177  cxpaddlelem  25338  mule1  25731  ppiub  25786  dchrabs2  25844  bposlem1  25866  zabsle1  25878  lgseisen  25961  lgsquadlem2  25963  rpvmasumlem  26069  qabvle  26207  ostth3  26220  colinearalg  26702  eengstr  26772  clwwlknon1le1  27884  eucrct2eupth  28028  nmosetn0  28546  nmoo0  28572  siii  28634  bcsiALT  28960  branmfn  29886  esumrnmpt2  31354  ballotlemrc  31815  pthhashvtx  32401  subfacval3  32463  sconnpi1  32513  fz0n  32989  poimirlem31  35000  itg2addnclem  35020  ftc1anc  35050  radcnvrat  40878  infxr  41865  stoweidlem18  42526  stoweidlem55  42563  fourierdlem62  42676  fourierswlem  42738  exple2lt6  44631
 Copyright terms: Public domain W3C validator