Theorem eqbrtrdi 5105

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  eqbrtrrdi  5106  domunsn  8667  mapdom1  8682  mapdom2  8688  pm54.43  9429  infmap2  9640  inar1  10197  gruina  10240  nn0ledivnn  12503  xltnegi  12610  leexp1a  13540  discr  13602  facwordi  13650  faclbnd3  13653  hashgt12el  13784  hashle2pr  13836  cnpart  14599  geomulcvg  15232  dvds1  15669  ramz2  16360  ramz  16361  gex1  18716  sylow2a  18744  en1top  21592  en2top  21593  hmph0  22403  ptcmplem2  22661  dscmet  23182  dscopn  23183  xrge0tsms2  23443  htpycc  23584  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  vitalilem5  24213  dvef  24577  dveq0  24597  dv11cn  24598  deg1lt0  24685  ply1rem  24757  fta1g  24761  plyremlem  24893  aalioulem3  24923  pige3ALT  25105  relogrn  25145  logneg  25171  cxpaddlelem  25332  mule1  25725  ppiub  25780  dchrabs2  25838  bposlem1  25860  zabsle1  25872  lgseisen  25955  lgsquadlem2  25957  rpvmasumlem  26063  qabvle  26201  ostth3  26214  colinearalg  26696  eengstr  26766  clwwlknon1le1  27880  eucrct2eupth  28024  nmosetn0  28542  nmoo0  28568  siii  28630  bcsiALT  28956  branmfn  29882  esumrnmpt2  31327  ballotlemrc  31788  pthhashvtx  32374  subfacval3  32436  sconnpi1  32486  fz0n  32962  poimirlem31  34938  itg2addnclem  34958  ftc1anc  34990  radcnvrat  40695  infxr  41684  stoweidlem18  42352  stoweidlem55  42389  fourierdlem62  42502  fourierswlem  42564  exple2lt6  44461