Theorem eqbrtrdi 5135

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  eqbrtrrdi  5136  domunsn  9053  mapdom1  9068  mapdom2  9074  pm54.43  9911  infmap2  10125  inar1  10684  gruina  10727  nn0ledivnn  13018  xltnegi  13129  leexp1a  14096  discr  14161  facwordi  14210  faclbnd3  14213  hashgt12el  14343  hashle2pr  14398  cnpart  15161  geomulcvg  15797  dvds1  16244  ramz2  16950  ramz  16951  gex1  19518  sylow2a  19546  en1top  22926  en2top  22927  hmph0  23737  ptcmplem2  23995  dscmet  24514  dscopn  24515  xrge0tsms2  24778  htpycc  24933  pcohtpylem  24973  pcopt  24976  pcopt2  24977  pcoass  24978  pcorevlem  24980  vitalilem5  25567  dvef  25938  dveq0  25959  dv11cn  25960  deg1lt0  26050  ply1rem  26125  fta1g  26129  plyremlem  26266  aalioulem3  26296  pige3ALT  26483  relogrn  26524  logneg  26551  cxpaddlelem  26715  mule1  27112  ppiub  27169  dchrabs2  27227  bposlem1  27249  zabsle1  27261  lgseisen  27344  lgsquadlem2  27346  rpvmasumlem  27452  qabvle  27590  ostth3  27603  precsexlem9  28183  nnsrecgt0d  28311  colinearalg  28932  eengstr  29002  clwwlknon1le1  30125  eucrct2eupth  30269  nmosetn0  30789  nmoo0  30815  siii  30877  bcsiALT  31203  branmfn  32129  fzo0opth  32832  drngidlhash  33464  m1pmeq  33615  cos9thpiminplylem1  33888  esumrnmpt2  34174  ballotlemrc  34637  pthhashvtx  35271  subfacval3  35332  sconnpi1  35382  fz0n  35874  poimirlem31  37791  itg2addnclem  37811  ftc1anc  37841  safesnsupfidom1o  43600  radcnvrat  44497  infxr  45553  stoweidlem18  46204  stoweidlem55  46241  fourierdlem62  46354  fourierswlem  46416  chnsubseqwl  47065  exple2lt6  48552  fvconstdomi  49079  f1omoALT  49082  indthincALT  49650