Theorem eqbrtrdi 5069

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  eqbrtrrdi  5070  domunsn  8651  mapdom1  8666  mapdom2  8672  pm54.43  9414  infmap2  9629  inar1  10186  gruina  10229  nn0ledivnn  12490  xltnegi  12597  leexp1a  13535  discr  13597  facwordi  13645  faclbnd3  13648  hashgt12el  13779  hashle2pr  13831  cnpart  14591  geomulcvg  15224  dvds1  15661  ramz2  16350  ramz  16351  gex1  18708  sylow2a  18736  en1top  21589  en2top  21590  hmph0  22400  ptcmplem2  22658  dscmet  23179  dscopn  23180  xrge0tsms2  23440  htpycc  23585  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  vitalilem5  24216  dvef  24583  dveq0  24603  dv11cn  24604  deg1lt0  24692  ply1rem  24764  fta1g  24768  plyremlem  24900  aalioulem3  24930  pige3ALT  25112  relogrn  25153  logneg  25179  cxpaddlelem  25340  mule1  25733  ppiub  25788  dchrabs2  25846  bposlem1  25868  zabsle1  25880  lgseisen  25963  lgsquadlem2  25965  rpvmasumlem  26071  qabvle  26209  ostth3  26222  colinearalg  26704  eengstr  26774  clwwlknon1le1  27886  eucrct2eupth  28030  nmosetn0  28548  nmoo0  28574  siii  28636  bcsiALT  28962  branmfn  29888  esumrnmpt2  31437  ballotlemrc  31898  pthhashvtx  32487  subfacval3  32549  sconnpi1  32599  fz0n  33075  poimirlem31  35088  itg2addnclem  35108  ftc1anc  35138  radcnvrat  41018  infxr  41999  stoweidlem18  42660  stoweidlem55  42697  fourierdlem62  42810  fourierswlem  42872  exple2lt6  44766