Theorem eqbrtrdi 5154

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  eqbrtrrdi  5155  domunsn  9114  mapdom1  9129  mapdom2  9135  pm54.43  9986  infmap2  10199  inar1  10759  gruina  10802  nn0ledivnn  13130  xltnegi  13241  leexp1a  14210  discr  14275  facwordi  14324  faclbnd3  14327  hashgt12el  14458  hashle2pr  14513  cnpart  15290  geomulcvg  15929  dvds1  16376  ramz2  17083  ramz  17084  gex1  19660  sylow2a  19688  en1top  23109  en2top  23110  hmph0  23920  ptcmplem2  24178  dscmet  24697  dscopn  24698  xrge0tsms2  24961  htpycc  25107  pcohtpylem  25146  pcopt  25149  pcopt2  25150  pcoass  25151  pcorevlem  25153  vitalilem5  25739  dvef  26107  dveq0  26127  dv11cn  26128  deg1lt0  26216  ply1rem  26291  fta1g  26295  plyremlem  26433  aalioulem3  26463  pige3ALT  26650  relogrn  26691  logneg  26718  cxpaddlelem  26881  mule1  27277  ppiub  27333  dchrabs2  27391  bposlem1  27413  zabsle1  27425  lgseisen  27508  lgsquadlem2  27510  rpvmasumlem  27616  qabvle  27754  ostth3  27767  precsexlem9  28373  nnsrecgt0d  28509  colinearalg  29200  eengstr  29270  clwwlknon1le1  30392  eucrct2eupth  30536  nmosetn0  31057  nmoo0  31083  siii  31145  bcsiALT  31471  branmfn  32397  fzo0opth  33088  drngidlhash  33685  fldlring  33733  m1pmeq  33819  cos9thpiminplylem1  34116  esumrnmpt2  34402  ballotlemrc  34865  pthhashvtx  35518  subfacval3  35579  sconnpi1  35629  fz0n  36121  poimirlem31  38189  itg2addnclem  38209  ftc1anc  38239  safesnsupfidom1o  44034  radcnvrat  44915  infxr  45973  stoweidlem18  46623  stoweidlem55  46660  fourierdlem62  46773  fourierswlem  46835  chnsubseqwl  47486  exple2lt6  49028  fvconstdomi  49554  f1omoALT  49557  indthincALT  50125