Theorem eqbrtrdi 5187

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5148

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  eqbrtrrdi  5188  domunsn  9129  mapdom1  9144  mapdom2  9150  pm54.43  9998  infmap2  10215  inar1  10772  gruina  10815  nn0ledivnn  13089  xltnegi  13197  leexp1a  14142  discr  14205  facwordi  14251  faclbnd3  14254  hashgt12el  14384  hashle2pr  14440  cnpart  15189  geomulcvg  15824  dvds1  16264  ramz2  16959  ramz  16960  gex1  19461  sylow2a  19489  en1top  22494  en2top  22495  hmph0  23306  ptcmplem2  23564  dscmet  24088  dscopn  24089  xrge0tsms2  24358  htpycc  24503  pcohtpylem  24542  pcopt  24545  pcopt2  24546  pcoass  24547  pcorevlem  24549  vitalilem5  25136  dvef  25504  dveq0  25524  dv11cn  25525  deg1lt0  25616  ply1rem  25688  fta1g  25692  plyremlem  25824  aalioulem3  25854  pige3ALT  26036  relogrn  26077  logneg  26103  cxpaddlelem  26266  mule1  26659  ppiub  26714  dchrabs2  26772  bposlem1  26794  zabsle1  26806  lgseisen  26889  lgsquadlem2  26891  rpvmasumlem  26997  qabvle  27135  ostth3  27148  precsexlem9  27671  colinearalg  28206  eengstr  28276  clwwlknon1le1  29392  eucrct2eupth  29536  nmosetn0  30056  nmoo0  30082  siii  30144  bcsiALT  30470  branmfn  31396  drngidlhash  32597  esumrnmpt2  33135  ballotlemrc  33598  pthhashvtx  34187  subfacval3  34249  sconnpi1  34299  fz0n  34769  poimirlem31  36605  itg2addnclem  36625  ftc1anc  36655  safesnsupfidom1o  42250  radcnvrat  43155  infxr  44156  stoweidlem18  44813  stoweidlem55  44850  fourierdlem62  44963  fourierswlem  45025  exple2lt6  47119  fvconstdomi  47604  f1omoALT  47606  indthincALT  47751