Theorem eqbrtrdi 5152

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  eqbrtrrdi  5153  domunsn  9122  mapdom1  9137  mapdom2  9143  pm54.43  10003  infmap2  10216  inar1  10775  gruina  10818  nn0ledivnn  13147  xltnegi  13258  leexp1a  14229  discr  14294  facwordi  14343  faclbnd3  14346  hashgt12el  14477  hashle2pr  14532  cnpart  15315  geomulcvg  15953  dvds1  16399  ramz2  17106  ramz  17107  gex1  19705  sylow2a  19733  en1top  23191  en2top  23192  hmph0  24003  ptcmplem2  24261  dscmet  24780  dscopn  24781  xrge0tsms2  25044  htpycc  25190  pcohtpylem  25229  pcopt  25232  pcopt2  25233  pcoass  25234  pcorevlem  25236  vitalilem5  25822  dvef  26190  dveq0  26210  dv11cn  26211  deg1lt0  26299  ply1rem  26374  fta1g  26378  plyremlem  26516  aalioulem3  26548  pige3ALT  26736  relogrn  26777  logneg  26804  cxpaddlelem  26967  mule1  27363  ppiub  27419  dchrabs2  27477  bposlem1  27499  zabsle1  27511  lgseisen  27594  lgsquadlem2  27596  rpvmasumlem  27702  qabvle  27840  ostth3  27853  precsexlem9  28459  nnsrecgt0d  28595  colinearalg  29315  eengstr  29385  pthhashvtx  30142  clwwlknon1le1  30519  eucrct2eupth  30667  nmosetn0  31188  nmoo0  31214  siii  31276  bcsiALT  31602  branmfn  32528  fzo0opth  33218  drngidlhash  33805  fldlring  33853  m1pmeq  33939  cos9thpiminplylem1  34236  esumrnmpt2  34522  ballotlemrc  34986  subfacval3  35718  sconnpi1  35768  fz0n  36260  poimirlem31  38359  itg2addnclem  38379  ftc1anc  38409  safesnsupfidom1o  44201  radcnvrat  45082  infxr  46140  stoweidlem18  46790  stoweidlem55  46827  fourierdlem62  46940  fourierswlem  47002  chnsubseqwl  47653  exple2lt6  49201  fvconstdomi  49727  f1omoALT  49730  indthincALT  50298