Theorem breqtrrdi 5127

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
breqtrrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrdi

Step	Hyp	Ref	Expression
1		breqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2745	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5126	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5085

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  enpr2d  8995  pw2eng  9021  undjudom  10090  dju1en  10094  djucomen  10100  djuassen  10101  xpdjuen  10102  infdjuabs  10127  ackbij1lem9  10149  unsnen  10475  1nqenq  10885  gtndiv  12606  xov1plusxeqvd  13451  intfrac2  13817  serle  14019  discr1  14201  faclbnd4lem1  14255  01sqrexlem1  15204  01sqrexlem4  15207  01sqrexlem7  15210  supcvg  15821  ege2le3  16055  eirrlem  16171  ruclem12  16208  bitsfzo  16404  pcprendvds  16811  pcpremul  16814  pcfaclem  16869  infpnlem2  16882  yonedainv  18247  srgbinomlem4  20210  lmcn2  23614  hmph0  23760  icccmplem2  24789  reconnlem2  24793  xrge0tsms  24800  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  ivthlem2  25419  ivthlem3  25420  vitalilem2  25576  itg2seq  25709  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  dveflem  25946  dvferm1lem  25951  dvferm2lem  25953  c1liplem1  25963  lhop1lem  25980  dvcvx  25987  plyeq0lem  26175  radcnvcl  26382  radcnvle  26385  psercnlem1  26390  psercn  26391  pilem3  26418  tangtx  26469  cos02pilt1  26490  cosne0  26493  recosf1o  26499  resinf1o  26500  efif1olem4  26509  logi  26551  logimul  26578  logcnlem3  26608  logf1o2  26614  ang180lem2  26774  heron  26802  acoscos  26857  emcllem7  26965  fsumharmonic  26975  ftalem2  27037  basellem1  27044  basellem2  27045  basellem3  27046  basellem5  27048  bposlem1  27247  bposlem2  27248  bposlem3  27249  lgsdirprm  27294  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  mulog2sumlem2  27498  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntlemc  27558  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemr  27565  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth3  27601  axsegconlem3  28988  clwlkclwwlk2  30073  siilem1  30922  minvecolem2  30946  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  nmopcoi  32166  staddi  32317  cycpmco2lem4  33190  cycpmco2lem5  33191  iconstr  33910  hgt750lemd  34792  climlec3  35916  poimirlem26  37967  ftc1anclem8  38021  cntotbnd  38117  dalemply  40100  dalemsly  40101  dalem5  40113  dalem13  40122  dalem17  40126  dalem55  40173  dalem57  40175  lhpat3  40492  cdleme22aa  40785  aks4d1p1p7  42513  evlselv  43020  jm2.27c  43435  hashnzfz2  44748  supxrubd  45543  suprnmpt  45604  fzisoeu  45733  upbdrech  45738  recnnltrp  45806  uzublem  45858  fmul01  46010  limsupubuzlem  46140  limsupequzmptlem  46156  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem36  46464  stoweidlem41  46469  wallispi2  46501  dirkercncflem1  46531  fourierdlem6  46541  fourierdlem7  46542  fourierdlem19  46554  fourierdlem20  46555  fourierdlem24  46559  fourierdlem25  46560  fourierdlem26  46561  fourierdlem30  46565  fourierdlem31  46566  fourierdlem42  46577  fourierdlem47  46581  fourierdlem48  46582  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem71  46605  fourierdlem79  46613  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fouriersw  46659  etransclem28  46690  etransclem48  46710  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem4  47026  bgoldbtbndlem2  48282  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  lincresunit3lem2  48956  lincresunit3  48957  resum2sqgt0  49183  amgmwlem  50277