Theorem eqbrtrdi 5111

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  eqbrtrrdi  5112  domunsn  9055  mapdom1  9070  mapdom2  9076  pm54.43  9916  infmap2  10130  inar1  10689  gruina  10732  nn0ledivnn  13048  xltnegi  13159  leexp1a  14128  discr  14193  facwordi  14242  faclbnd3  14245  hashgt12el  14375  hashle2pr  14430  cnpart  15193  geomulcvg  15832  dvds1  16279  ramz2  16986  ramz  16987  gex1  19557  sylow2a  19585  en1top  22967  en2top  22968  hmph0  23778  ptcmplem2  24036  dscmet  24555  dscopn  24556  xrge0tsms2  24819  htpycc  24965  pcohtpylem  25004  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevlem  25011  vitalilem5  25597  dvef  25965  dveq0  25985  dv11cn  25986  deg1lt0  26074  ply1rem  26149  fta1g  26153  plyremlem  26288  aalioulem3  26318  pige3ALT  26502  relogrn  26543  logneg  26570  cxpaddlelem  26733  mule1  27129  ppiub  27185  dchrabs2  27243  bposlem1  27265  zabsle1  27277  lgseisen  27360  lgsquadlem2  27362  rpvmasumlem  27468  qabvle  27606  ostth3  27619  precsexlem9  28225  nnsrecgt0d  28361  colinearalg  28997  eengstr  29067  clwwlknon1le1  30189  eucrct2eupth  30333  nmosetn0  30854  nmoo0  30880  siii  30942  bcsiALT  31268  branmfn  32194  fzo0opth  32895  drngidlhash  33517  m1pmeq  33668  cos9thpiminplylem1  33966  esumrnmpt2  34252  ballotlemrc  34715  pthhashvtx  35356  subfacval3  35417  sconnpi1  35467  fz0n  35959  poimirlem31  38018  itg2addnclem  38038  ftc1anc  38068  safesnsupfidom1o  43861  radcnvrat  44758  infxr  45811  stoweidlem18  46461  stoweidlem55  46498  fourierdlem62  46611  fourierswlem  46673  chnsubseqwl  47324  exple2lt6  48855  fvconstdomi  49382  f1omoALT  49385  indthincALT  49953