Theorem eqbrtrdi 5188

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  eqbrtrrdi  5189  domunsn  9127  mapdom1  9142  mapdom2  9148  pm54.43  9996  infmap2  10213  inar1  10770  gruina  10813  nn0ledivnn  13087  xltnegi  13195  leexp1a  14140  discr  14203  facwordi  14249  faclbnd3  14252  hashgt12el  14382  hashle2pr  14438  cnpart  15187  geomulcvg  15822  dvds1  16262  ramz2  16957  ramz  16958  gex1  19459  sylow2a  19487  en1top  22487  en2top  22488  hmph0  23299  ptcmplem2  23557  dscmet  24081  dscopn  24082  xrge0tsms2  24351  htpycc  24496  pcohtpylem  24535  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  vitalilem5  25129  dvef  25497  dveq0  25517  dv11cn  25518  deg1lt0  25609  ply1rem  25681  fta1g  25685  plyremlem  25817  aalioulem3  25847  pige3ALT  26029  relogrn  26070  logneg  26096  cxpaddlelem  26259  mule1  26652  ppiub  26707  dchrabs2  26765  bposlem1  26787  zabsle1  26799  lgseisen  26882  lgsquadlem2  26884  rpvmasumlem  26990  qabvle  27128  ostth3  27141  precsexlem9  27661  colinearalg  28168  eengstr  28238  clwwlknon1le1  29354  eucrct2eupth  29498  nmosetn0  30018  nmoo0  30044  siii  30106  bcsiALT  30432  branmfn  31358  drngidlhash  32552  esumrnmpt2  33066  ballotlemrc  33529  pthhashvtx  34118  subfacval3  34180  sconnpi1  34230  fz0n  34700  poimirlem31  36519  itg2addnclem  36539  ftc1anc  36569  safesnsupfidom1o  42168  radcnvrat  43073  infxr  44077  stoweidlem18  44734  stoweidlem55  44771  fourierdlem62  44884  fourierswlem  44946  exple2lt6  47040  fvconstdomi  47526  f1omoALT  47528  indthincALT  47673