Theorem breqtrrdi 5147

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  enpr2d  9055  pw2eng  9081  undjudom  10203  dju1en  10207  djucomen  10213  djuassen  10214  xpdjuen  10215  infdjuabs  10240  ackbij1lem9  10262  unsnen  10594  1nqenq  11004  gtndiv  12731  xov1plusxeqvd  13584  intfrac2  13952  serle  14154  discr1  14336  faclbnd4lem1  14390  01sqrexlem1  15362  01sqrexlem4  15365  01sqrexlem7  15368  supcvg  15978  ege2le3  16209  eirrlem  16325  ruclem12  16362  bitsfzo  16558  pcprendvds  16965  pcpremul  16968  pcfaclem  17023  infpnlem2  17036  yonedainv  18402  srgbinomlem4  20402  lmcn2  23915  hmph0  24061  icccmplem2  25090  reconnlem2  25094  xrge0tsms  25101  minveclem2  25694  minveclem3b  25696  minveclem4  25700  minveclem6  25702  ivthlem2  25720  ivthlem3  25721  vitalilem2  25877  itg2seq  26010  itg2monolem1  26018  itg2monolem2  26019  itg2monolem3  26020  dveflem  26246  dvferm1lem  26251  dvferm2lem  26253  c1liplem1  26263  lhop1lem  26280  dvcvx  26287  plyeq0lem  26476  radcnvcl  26693  radcnvle  26696  psercnlem1  26701  psercn  26702  pilem3  26729  tangtx  26783  cos02pilt1  26803  cosne0  26806  recosf1o  26812  resinf1o  26813  efif1olem4  26822  logi  26864  logimul  26891  logcnlem3  26921  logf1o2  26927  ang180lem2  27087  heron  27115  acoscos  27170  emcllem7  27278  fsumharmonic  27288  ftalem2  27350  basellem1  27357  basellem2  27358  basellem3  27359  basellem5  27361  bposlem1  27560  bposlem2  27561  bposlem3  27562  lgsdirprm  27607  chebbnd1lem1  27745  chebbnd1lem2  27746  chebbnd1lem3  27747  mulog2sumlem2  27811  pntpbnd1a  27861  pntpbnd1  27862  pntpbnd2  27863  pntibndlem2  27867  pntlemc  27871  pntlemb  27873  pntlemg  27874  pntlemh  27875  pntlemr  27878  ostth2lem2  27910  ostth2lem3  27911  ostth2lem4  27912  ostth3  27914  axsegconlem3  29416  clwlkclwwlk2  30513  siilem1  31372  minvecolem2  31396  minvecolem4  31401  minvecolem5  31402  minvecolem6  31403  nmopcoi  32616  staddi  32767  cycpmco2lem4  33609  cycpmco2lem5  33610  iconstr  34317  hgt750lemd  35197  climlec3  36414  poimirlem26  38478  ftc1anclem8  38532  cntotbnd  38644  dalemply  40625  dalemsly  40626  dalem5  40638  dalem13  40647  dalem17  40651  dalem55  40698  dalem57  40700  lhpat3  41017  cdleme22aa  41310  aks4d1p1p7  43038  evlselv  43533  jm2.27c  43946  hashnzfz2  45243  supxrubd  46043  suprnmpt  46104  fzisoeu  46231  upbdrech  46236  recnnltrp  46304  uzublem  46356  fmul01  46508  limsupubuzlem  46638  limsupequzmptlem  46654  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  stoweidlem36  46962  stoweidlem41  46967  wallispi2  46999  dirkercncflem1  47029  fourierdlem6  47039  fourierdlem7  47040  fourierdlem19  47052  fourierdlem20  47053  fourierdlem24  47057  fourierdlem25  47058  fourierdlem26  47059  fourierdlem30  47063  fourierdlem31  47064  fourierdlem42  47075  fourierdlem47  47079  fourierdlem48  47080  fourierdlem49  47081  fourierdlem63  47095  fourierdlem64  47096  fourierdlem65  47097  fourierdlem71  47103  fourierdlem79  47111  fourierdlem89  47121  fourierdlem90  47122  fourierdlem91  47123  fouriersw  47157  etransclem28  47188  etransclem48  47208  hoidmv1lelem1  47517  hoidmv1lelem3  47519  hoidmvlelem1  47521  hoidmvlelem4  47524  bgoldbtbndlem2  48820  gpg3kgrtriexlem4  49100  gpg3kgrtriexlem6  49102  lincresunit3lem2  49508  lincresunit3  49509  resum2sqgt0  49735  amgmwlem  50903