Theorem eqbrtrdi 5125

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtrrdi  5126  domunsn  9056  mapdom1  9071  mapdom2  9077  pm54.43  9914  infmap2  10128  inar1  10687  gruina  10730  nn0ledivnn  13046  xltnegi  13157  leexp1a  14126  discr  14191  facwordi  14240  faclbnd3  14243  hashgt12el  14373  hashle2pr  14428  cnpart  15191  geomulcvg  15830  dvds1  16277  ramz2  16984  ramz  16985  gex1  19555  sylow2a  19583  en1top  22957  en2top  22958  hmph0  23768  ptcmplem2  24026  dscmet  24545  dscopn  24546  xrge0tsms2  24809  htpycc  24955  pcohtpylem  24994  pcopt  24997  pcopt2  24998  pcoass  24999  pcorevlem  25001  vitalilem5  25587  dvef  25955  dveq0  25975  dv11cn  25976  deg1lt0  26064  ply1rem  26139  fta1g  26143  plyremlem  26279  aalioulem3  26309  pige3ALT  26495  relogrn  26536  logneg  26563  cxpaddlelem  26726  mule1  27123  ppiub  27179  dchrabs2  27237  bposlem1  27259  zabsle1  27271  lgseisen  27354  lgsquadlem2  27356  rpvmasumlem  27462  qabvle  27600  ostth3  27613  precsexlem9  28219  nnsrecgt0d  28355  colinearalg  28991  eengstr  29061  clwwlknon1le1  30184  eucrct2eupth  30328  nmosetn0  30849  nmoo0  30875  siii  30937  bcsiALT  31263  branmfn  32189  fzo0opth  32889  drngidlhash  33507  m1pmeq  33658  cos9thpiminplylem1  33940  esumrnmpt2  34226  ballotlemrc  34689  pthhashvtx  35324  subfacval3  35385  sconnpi1  35435  fz0n  35927  poimirlem31  37976  itg2addnclem  37996  ftc1anc  38026  safesnsupfidom1o  43852  radcnvrat  44749  infxr  45804  stoweidlem18  46454  stoweidlem55  46491  fourierdlem62  46604  fourierswlem  46666  chnsubseqwl  47315  exple2lt6  48842  fvconstdomi  49369  f1omoALT  49372  indthincALT  49940