Theorem eqbrtrdi 5191

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

Syntax hints:   → wi 4   = wceq 1533   class class class wbr 5152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153

This theorem is referenced by:  eqbrtrrdi  5192  domunsn  9158  mapdom1  9173  mapdom2  9179  pm54.43  10032  infmap2  10249  inar1  10806  gruina  10849  nn0ledivnn  13127  xltnegi  13235  leexp1a  14179  discr  14242  facwordi  14288  faclbnd3  14291  hashgt12el  14421  hashle2pr  14478  cnpart  15227  geomulcvg  15862  dvds1  16303  ramz2  17000  ramz  17001  gex1  19553  sylow2a  19581  en1top  22907  en2top  22908  hmph0  23719  ptcmplem2  23977  dscmet  24501  dscopn  24502  xrge0tsms2  24771  htpycc  24926  pcohtpylem  24966  pcopt  24969  pcopt2  24970  pcoass  24971  pcorevlem  24973  vitalilem5  25561  dvef  25932  dveq0  25953  dv11cn  25954  deg1lt0  26047  ply1rem  26120  fta1g  26124  plyremlem  26259  aalioulem3  26289  pige3ALT  26474  relogrn  26515  logneg  26542  cxpaddlelem  26706  mule1  27100  ppiub  27157  dchrabs2  27215  bposlem1  27237  zabsle1  27249  lgseisen  27332  lgsquadlem2  27334  rpvmasumlem  27440  qabvle  27578  ostth3  27591  precsexlem9  28133  nnsrecgt0d  28239  0reno  28245  colinearalg  28741  eengstr  28811  clwwlknon1le1  29931  eucrct2eupth  30075  nmosetn0  30595  nmoo0  30621  siii  30683  bcsiALT  31009  branmfn  31935  drngidlhash  33175  m1pmeq  33294  esumrnmpt2  33720  ballotlemrc  34183  pthhashvtx  34770  subfacval3  34832  sconnpi1  34882  fz0n  35358  poimirlem31  37157  itg2addnclem  37177  ftc1anc  37207  safesnsupfidom1o  42878  radcnvrat  43782  infxr  44778  stoweidlem18  45435  stoweidlem55  45472  fourierdlem62  45585  fourierswlem  45647  exple2lt6  47506  fvconstdomi  47990  f1omoALT  47992  indthincALT  48137