Theorem eqbrtrdi 5149

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5110

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  eqbrtrrdi  5150  domunsn  9078  mapdom1  9093  mapdom2  9099  pm54.43  9946  infmap2  10163  inar1  10720  gruina  10763  nn0ledivnn  13037  xltnegi  13145  leexp1a  14090  discr  14153  facwordi  14199  faclbnd3  14202  hashgt12el  14332  hashle2pr  14388  cnpart  15137  geomulcvg  15772  dvds1  16212  ramz2  16907  ramz  16908  gex1  19387  sylow2a  19415  en1top  22371  en2top  22372  hmph0  23183  ptcmplem2  23441  dscmet  23965  dscopn  23966  xrge0tsms2  24235  htpycc  24380  pcohtpylem  24419  pcopt  24422  pcopt2  24423  pcoass  24424  pcorevlem  24426  vitalilem5  25013  dvef  25381  dveq0  25401  dv11cn  25402  deg1lt0  25493  ply1rem  25565  fta1g  25569  plyremlem  25701  aalioulem3  25731  pige3ALT  25913  relogrn  25954  logneg  25980  cxpaddlelem  26141  mule1  26534  ppiub  26589  dchrabs2  26647  bposlem1  26669  zabsle1  26681  lgseisen  26764  lgsquadlem2  26766  rpvmasumlem  26872  qabvle  27010  ostth3  27023  colinearalg  27922  eengstr  27992  clwwlknon1le1  29108  eucrct2eupth  29252  nmosetn0  29770  nmoo0  29796  siii  29858  bcsiALT  30184  branmfn  31110  esumrnmpt2  32756  ballotlemrc  33219  pthhashvtx  33808  subfacval3  33870  sconnpi1  33920  fz0n  34389  poimirlem31  36182  itg2addnclem  36202  ftc1anc  36232  safesnsupfidom1o  41811  radcnvrat  42716  infxr  43722  stoweidlem18  44379  stoweidlem55  44416  fourierdlem62  44529  fourierswlem  44591  exple2lt6  46560  fvconstdomi  47046  f1omoALT  47048  indthincALT  47193