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  9139  mapdom1  9154  mapdom2  9160  pm54.43  10013  infmap2  10229  inar1  10787  gruina  10830  nn0ledivnn  13120  xltnegi  13230  leexp1a  14191  discr  14256  facwordi  14305  faclbnd3  14308  hashgt12el  14438  hashle2pr  14493  cnpart  15257  geomulcvg  15890  dvds1  16336  ramz2  17042  ramz  17043  gex1  19570  sylow2a  19598  en1top  22920  en2top  22921  hmph0  23731  ptcmplem2  23989  dscmet  24509  dscopn  24510  xrge0tsms2  24773  htpycc  24928  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  vitalilem5  25563  dvef  25934  dveq0  25955  dv11cn  25956  deg1lt0  26046  ply1rem  26121  fta1g  26125  plyremlem  26262  aalioulem3  26292  pige3ALT  26479  relogrn  26520  logneg  26547  cxpaddlelem  26711  mule1  27108  ppiub  27165  dchrabs2  27223  bposlem1  27245  zabsle1  27257  lgseisen  27340  lgsquadlem2  27342  rpvmasumlem  27448  qabvle  27586  ostth3  27599  precsexlem9  28156  nnsrecgt0d  28273  cutpw2  28334  pw2bday  28335  0reno  28346  colinearalg  28835  eengstr  28905  clwwlknon1le1  30028  eucrct2eupth  30172  nmosetn0  30692  nmoo0  30718  siii  30780  bcsiALT  31106  branmfn  32032  fzo0opth  32728  drngidlhash  33395  m1pmeq  33542  cos9thpiminplylem1  33762  esumrnmpt2  34045  ballotlemrc  34509  pthhashvtx  35096  subfacval3  35157  sconnpi1  35207  fz0n  35694  poimirlem31  37621  itg2addnclem  37641  ftc1anc  37671  safesnsupfidom1o  43388  radcnvrat  44286  infxr  45342  stoweidlem18  45995  stoweidlem55  46032  fourierdlem62  46145  fourierswlem  46207  exple2lt6  48287  fvconstdomi  48815  f1omoALT  48817  indthincALT  49297