Theorem eqbrtrdi 5158

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

Step	Hyp	Ref	Expression
1		eqbrtrdi.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtrdi.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5129	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 258	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  eqbrtrrdi  5159  domunsn  9141  mapdom1  9156  mapdom2  9162  pm54.43  10015  infmap2  10231  inar1  10789  gruina  10832  nn0ledivnn  13122  xltnegi  13232  leexp1a  14193  discr  14258  facwordi  14307  faclbnd3  14310  hashgt12el  14440  hashle2pr  14495  cnpart  15259  geomulcvg  15892  dvds1  16338  ramz2  17044  ramz  17045  gex1  19572  sylow2a  19600  en1top  22922  en2top  22923  hmph0  23733  ptcmplem2  23991  dscmet  24511  dscopn  24512  xrge0tsms2  24775  htpycc  24930  pcohtpylem  24970  pcopt  24973  pcopt2  24974  pcoass  24975  pcorevlem  24977  vitalilem5  25565  dvef  25936  dveq0  25957  dv11cn  25958  deg1lt0  26048  ply1rem  26123  fta1g  26127  plyremlem  26264  aalioulem3  26294  pige3ALT  26481  relogrn  26522  logneg  26549  cxpaddlelem  26713  mule1  27110  ppiub  27167  dchrabs2  27225  bposlem1  27247  zabsle1  27259  lgseisen  27342  lgsquadlem2  27344  rpvmasumlem  27450  qabvle  27588  ostth3  27601  precsexlem9  28169  nnsrecgt0d  28295  0reno  28400  colinearalg  28889  eengstr  28959  clwwlknon1le1  30082  eucrct2eupth  30226  nmosetn0  30746  nmoo0  30772  siii  30834  bcsiALT  31160  branmfn  32086  fzo0opth  32782  drngidlhash  33449  m1pmeq  33596  cos9thpiminplylem1  33816  esumrnmpt2  34099  ballotlemrc  34563  pthhashvtx  35150  subfacval3  35211  sconnpi1  35261  fz0n  35748  poimirlem31  37675  itg2addnclem  37695  ftc1anc  37725  safesnsupfidom1o  43441  radcnvrat  44338  infxr  45394  stoweidlem18  46047  stoweidlem55  46084  fourierdlem62  46197  fourierswlem  46259  exple2lt6  48339  fvconstdomi  48867  f1omoALT  48869  indthincALT  49349