Theorem breqtrrdi 5128

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 2746	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5127	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  enpr2d  8990  pw2eng  9016  undjudom  10085  dju1en  10089  djucomen  10095  djuassen  10096  xpdjuen  10097  infdjuabs  10122  ackbij1lem9  10144  unsnen  10470  1nqenq  10880  gtndiv  12601  xov1plusxeqvd  13446  intfrac2  13812  serle  14014  discr1  14196  faclbnd4lem1  14250  01sqrexlem1  15199  01sqrexlem4  15202  01sqrexlem7  15205  supcvg  15816  ege2le3  16050  eirrlem  16166  ruclem12  16203  bitsfzo  16399  pcprendvds  16806  pcpremul  16809  pcfaclem  16864  infpnlem2  16877  yonedainv  18242  srgbinomlem4  20205  lmcn2  23628  hmph0  23774  icccmplem2  24803  reconnlem2  24807  xrge0tsms  24814  minveclem2  25407  minveclem3b  25409  minveclem4  25413  minveclem6  25415  ivthlem2  25433  ivthlem3  25434  vitalilem2  25590  itg2seq  25723  itg2monolem1  25731  itg2monolem2  25732  itg2monolem3  25733  dveflem  25960  dvferm1lem  25965  dvferm2lem  25967  c1liplem1  25977  lhop1lem  25994  dvcvx  26001  plyeq0lem  26189  radcnvcl  26399  radcnvle  26402  psercnlem1  26407  psercn  26408  pilem3  26435  tangtx  26486  cos02pilt1  26507  cosne0  26510  recosf1o  26516  resinf1o  26517  efif1olem4  26526  logi  26568  logimul  26595  logcnlem3  26625  logf1o2  26631  ang180lem2  26791  heron  26819  acoscos  26874  emcllem7  26983  fsumharmonic  26993  ftalem2  27055  basellem1  27062  basellem2  27063  basellem3  27064  basellem5  27066  bposlem1  27265  bposlem2  27266  bposlem3  27267  lgsdirprm  27312  chebbnd1lem1  27450  chebbnd1lem2  27451  chebbnd1lem3  27452  mulog2sumlem2  27516  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2  27572  pntlemc  27576  pntlemb  27578  pntlemg  27579  pntlemh  27580  pntlemr  27583  ostth2lem2  27615  ostth2lem3  27616  ostth2lem4  27617  ostth3  27619  axsegconlem3  29006  clwlkclwwlk2  30092  siilem1  30941  minvecolem2  30965  minvecolem4  30970  minvecolem5  30971  minvecolem6  30972  nmopcoi  32185  staddi  32336  cycpmco2lem4  33209  cycpmco2lem5  33210  iconstr  33930  hgt750lemd  34812  climlec3  35936  poimirlem26  37987  ftc1anclem8  38041  cntotbnd  38137  dalemply  40120  dalemsly  40121  dalem5  40133  dalem13  40142  dalem17  40146  dalem55  40193  dalem57  40195  lhpat3  40512  cdleme22aa  40805  aks4d1p1p7  42533  evlselv  43040  jm2.27c  43459  hashnzfz2  44772  supxrubd  45567  suprnmpt  45628  fzisoeu  45757  upbdrech  45762  recnnltrp  45830  uzublem  45882  fmul01  46034  limsupubuzlem  46164  limsupequzmptlem  46180  ioodvbdlimc1lem2  46384  ioodvbdlimc2lem  46386  stoweidlem36  46488  stoweidlem41  46493  wallispi2  46525  dirkercncflem1  46555  fourierdlem6  46565  fourierdlem7  46566  fourierdlem19  46578  fourierdlem20  46579  fourierdlem24  46583  fourierdlem25  46584  fourierdlem26  46585  fourierdlem30  46589  fourierdlem31  46590  fourierdlem42  46601  fourierdlem47  46605  fourierdlem48  46606  fourierdlem63  46621  fourierdlem64  46622  fourierdlem65  46623  fourierdlem71  46629  fourierdlem79  46637  fourierdlem89  46647  fourierdlem90  46648  fourierdlem91  46649  fouriersw  46683  etransclem28  46714  etransclem48  46734  hoidmv1lelem1  47043  hoidmv1lelem3  47045  hoidmvlelem1  47047  hoidmvlelem4  47050  bgoldbtbndlem2  48300  gpg3kgrtriexlem4  48580  gpg3kgrtriexlem6  48582  lincresunit3lem2  48974  lincresunit3  48975  resum2sqgt0  49201  amgmwlem  50295