Theorem eqbrtrdi 5113

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  eqbrtrrdi  5114  domunsn  8914  mapdom1  8929  mapdom2  8935  pm54.43  9759  infmap2  9974  inar1  10531  gruina  10574  nn0ledivnn  12843  xltnegi  12950  leexp1a  13893  discr  13955  facwordi  14003  faclbnd3  14006  hashgt12el  14137  hashle2pr  14191  cnpart  14951  geomulcvg  15588  dvds1  16028  ramz2  16725  ramz  16726  gex1  19196  sylow2a  19224  en1top  22134  en2top  22135  hmph0  22946  ptcmplem2  23204  dscmet  23728  dscopn  23729  xrge0tsms2  23998  htpycc  24143  pcohtpylem  24182  pcopt  24185  pcopt2  24186  pcoass  24187  pcorevlem  24189  vitalilem5  24776  dvef  25144  dveq0  25164  dv11cn  25165  deg1lt0  25256  ply1rem  25328  fta1g  25332  plyremlem  25464  aalioulem3  25494  pige3ALT  25676  relogrn  25717  logneg  25743  cxpaddlelem  25904  mule1  26297  ppiub  26352  dchrabs2  26410  bposlem1  26432  zabsle1  26444  lgseisen  26527  lgsquadlem2  26529  rpvmasumlem  26635  qabvle  26773  ostth3  26786  colinearalg  27278  eengstr  27348  clwwlknon1le1  28465  eucrct2eupth  28609  nmosetn0  29127  nmoo0  29153  siii  29215  bcsiALT  29541  branmfn  30467  esumrnmpt2  32036  ballotlemrc  32497  pthhashvtx  33089  subfacval3  33151  sconnpi1  33201  fz0n  33696  poimirlem31  35808  itg2addnclem  35828  ftc1anc  35858  radcnvrat  41932  infxr  42906  stoweidlem18  43559  stoweidlem55  43596  fourierdlem62  43709  fourierswlem  43771  exple2lt6  45700  fvconstdomi  46187  f1omoALT  46189  indthincALT  46334