MPE Home 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 1543   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 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054
This theorem is referenced by:  eqbrtrrdi  5093  domunsn  8796  mapdom1  8811  mapdom2  8817  pm54.43  9617  infmap2  9832  inar1  10389  gruina  10432  nn0ledivnn  12699  xltnegi  12806  leexp1a  13745  discr  13807  facwordi  13855  faclbnd3  13858  hashgt12el  13989  hashle2pr  14043  cnpart  14803  geomulcvg  15440  dvds1  15880  ramz2  16577  ramz  16578  gex1  18980  sylow2a  19008  en1top  21881  en2top  21882  hmph0  22692  ptcmplem2  22950  dscmet  23470  dscopn  23471  xrge0tsms2  23732  htpycc  23877  pcohtpylem  23916  pcopt  23919  pcopt2  23920  pcoass  23921  pcorevlem  23923  vitalilem5  24509  dvef  24877  dveq0  24897  dv11cn  24898  deg1lt0  24989  ply1rem  25061  fta1g  25065  plyremlem  25197  aalioulem3  25227  pige3ALT  25409  relogrn  25450  logneg  25476  cxpaddlelem  25637  mule1  26030  ppiub  26085  dchrabs2  26143  bposlem1  26165  zabsle1  26177  lgseisen  26260  lgsquadlem2  26262  rpvmasumlem  26368  qabvle  26506  ostth3  26519  colinearalg  27001  eengstr  27071  clwwlknon1le1  28184  eucrct2eupth  28328  nmosetn0  28846  nmoo0  28872  siii  28934  bcsiALT  29260  branmfn  30186  esumrnmpt2  31748  ballotlemrc  32209  pthhashvtx  32802  subfacval3  32864  sconnpi1  32914  fz0n  33414  poimirlem31  35545  itg2addnclem  35565  ftc1anc  35595  radcnvrat  41608  infxr  42582  stoweidlem18  43237  stoweidlem55  43274  fourierdlem62  43387  fourierswlem  43449  exple2lt6  45376  fvconstdomi  45863  f1omoALT  45865  indthincALT  46010
  Copyright terms: Public domain W3C validator