Theorem eqbrtrdi 5137

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

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

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  eqbrtrrdi  5138  domunsn  9055  mapdom1  9070  mapdom2  9076  pm54.43  9913  infmap2  10127  inar1  10686  gruina  10729  nn0ledivnn  13020  xltnegi  13131  leexp1a  14098  discr  14163  facwordi  14212  faclbnd3  14215  hashgt12el  14345  hashle2pr  14400  cnpart  15163  geomulcvg  15799  dvds1  16246  ramz2  16952  ramz  16953  gex1  19520  sylow2a  19548  en1top  22928  en2top  22929  hmph0  23739  ptcmplem2  23997  dscmet  24516  dscopn  24517  xrge0tsms2  24780  htpycc  24935  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  vitalilem5  25569  dvef  25940  dveq0  25961  dv11cn  25962  deg1lt0  26052  ply1rem  26127  fta1g  26131  plyremlem  26268  aalioulem3  26298  pige3ALT  26485  relogrn  26526  logneg  26553  cxpaddlelem  26717  mule1  27114  ppiub  27171  dchrabs2  27229  bposlem1  27251  zabsle1  27263  lgseisen  27346  lgsquadlem2  27348  rpvmasumlem  27454  qabvle  27592  ostth3  27605  precsexlem9  28211  nnsrecgt0d  28347  colinearalg  28983  eengstr  29053  clwwlknon1le1  30176  eucrct2eupth  30320  nmosetn0  30840  nmoo0  30866  siii  30928  bcsiALT  31254  branmfn  32180  fzo0opth  32883  drngidlhash  33515  m1pmeq  33666  cos9thpiminplylem1  33939  esumrnmpt2  34225  ballotlemrc  34688  pthhashvtx  35322  subfacval3  35383  sconnpi1  35433  fz0n  35925  poimirlem31  37852  itg2addnclem  37872  ftc1anc  37902  safesnsupfidom1o  43658  radcnvrat  44555  infxr  45611  stoweidlem18  46262  stoweidlem55  46299  fourierdlem62  46412  fourierswlem  46474  chnsubseqwl  47123  exple2lt6  48610  fvconstdomi  49137  f1omoALT  49140  indthincALT  49708