Theorem eqbrtrdi 5187

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 5158	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 258	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  eqbrtrrdi  5188  domunsn  9166  mapdom1  9181  mapdom2  9187  pm54.43  10039  infmap2  10255  inar1  10813  gruina  10856  nn0ledivnn  13146  xltnegi  13255  leexp1a  14212  discr  14276  facwordi  14325  faclbnd3  14328  hashgt12el  14458  hashle2pr  14513  cnpart  15276  geomulcvg  15909  dvds1  16353  ramz2  17058  ramz  17059  gex1  19624  sylow2a  19652  en1top  23007  en2top  23008  hmph0  23819  ptcmplem2  24077  dscmet  24601  dscopn  24602  xrge0tsms2  24871  htpycc  25026  pcohtpylem  25066  pcopt  25069  pcopt2  25070  pcoass  25071  pcorevlem  25073  vitalilem5  25661  dvef  26033  dveq0  26054  dv11cn  26055  deg1lt0  26145  ply1rem  26220  fta1g  26224  plyremlem  26361  aalioulem3  26391  pige3ALT  26577  relogrn  26618  logneg  26645  cxpaddlelem  26809  mule1  27206  ppiub  27263  dchrabs2  27321  bposlem1  27343  zabsle1  27355  lgseisen  27438  lgsquadlem2  27440  rpvmasumlem  27546  qabvle  27684  ostth3  27697  precsexlem9  28254  nnsrecgt0d  28371  cutpw2  28432  pw2bday  28433  0reno  28444  colinearalg  28940  eengstr  29010  clwwlknon1le1  30130  eucrct2eupth  30274  nmosetn0  30794  nmoo0  30820  siii  30882  bcsiALT  31208  branmfn  32134  fzo0opth  32813  drngidlhash  33442  m1pmeq  33588  esumrnmpt2  34049  ballotlemrc  34512  pthhashvtx  35112  subfacval3  35174  sconnpi1  35224  fz0n  35711  poimirlem31  37638  itg2addnclem  37658  ftc1anc  37688  safesnsupfidom1o  43407  radcnvrat  44310  infxr  45317  stoweidlem18  45974  stoweidlem55  46011  fourierdlem62  46124  fourierswlem  46186  exple2lt6  48209  fvconstdomi  48690  f1omoALT  48692  indthincALT  48854