Theorem breqtrrdi 5150

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  enpr2d  9101  pw2eng  9127  undjudom  10270  dju1en  10274  djucomen  10280  djuassen  10281  xpdjuen  10282  infdjuabs  10307  ackbij1lem9  10329  unsnen  10661  1nqenq  11071  gtndiv  12800  xov1plusxeqvd  13653  intfrac2  14022  serle  14224  discr1  14407  faclbnd4lem1  14461  01sqrexlem1  15435  01sqrexlem4  15438  01sqrexlem7  15441  supcvg  16051  ege2le3  16282  eirrlem  16398  ruclem12  16435  bitsfzo  16631  pcprendvds  17044  pcpremul  17047  pcfaclem  17102  infpnlem2  17115  yonedainv  18481  srgbinomlem4  20482  lmcn2  23995  hmph0  24141  icccmplem2  25170  reconnlem2  25174  xrge0tsms  25181  minveclem2  25774  minveclem3b  25776  minveclem4  25780  minveclem6  25782  ivthlem2  25800  ivthlem3  25801  vitalilem2  25957  itg2seq  26090  itg2monolem1  26098  itg2monolem2  26099  itg2monolem3  26100  dveflem  26326  dvferm1lem  26331  dvferm2lem  26333  c1liplem1  26343  lhop1lem  26360  dvcvx  26367  plyeq0lem  26556  radcnvcl  26771  radcnvle  26774  psercnlem1  26779  psercn  26780  pilem3  26807  tangtx  26861  cos02pilt1  26881  cosne0  26884  recosf1o  26890  resinf1o  26891  efif1olem4  26900  logi  26942  logimul  26969  logcnlem3  26999  logf1o2  27005  ang180lem2  27165  heron  27193  acoscos  27248  emcllem7  27356  fsumharmonic  27366  ftalem2  27428  basellem1  27435  basellem2  27436  basellem3  27437  basellem5  27439  bposlem1  27638  bposlem2  27639  bposlem3  27640  lgsdirprm  27685  chebbnd1lem1  27823  chebbnd1lem2  27824  chebbnd1lem3  27825  mulog2sumlem2  27889  pntpbnd1a  27939  pntpbnd1  27940  pntpbnd2  27941  pntibndlem2  27945  pntlemc  27949  pntlemb  27951  pntlemg  27952  pntlemh  27953  pntlemr  27956  ostth2lem2  27988  ostth2lem3  27989  ostth2lem4  27990  ostth3  27992  axsegconlem3  29524  clwlkclwwlk2  30621  siilem1  31480  minvecolem2  31504  minvecolem4  31509  minvecolem5  31510  minvecolem6  31511  nmopcoi  32724  staddi  32875  cycpmco2lem4  33757  cycpmco2lem5  33758  iconstr  34465  hgt750lemd  35344  climlec3  36676  poimirlem26  38755  ftc1anclem8  38809  cntotbnd  38921  dalemply  40902  dalemsly  40903  dalem5  40915  dalem13  40924  dalem17  40928  dalem55  40975  dalem57  40977  lhpat3  41294  cdleme22aa  41587  aks4d1p1p7  43315  evlselv  43808  jm2.27c  44205  hashnzfz2  45495  supxrubd  46331  suprnmpt  46392  fzisoeu  46519  upbdrech  46524  recnnltrp  46591  uzublem  46643  fmul01  46795  limsupubuzlem  46925  limsupequzmptlem  46941  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  stoweidlem36  47249  stoweidlem41  47254  wallispi2  47286  dirkercncflem1  47316  fourierdlem6  47326  fourierdlem7  47327  fourierdlem19  47339  fourierdlem20  47340  fourierdlem24  47344  fourierdlem25  47345  fourierdlem26  47346  fourierdlem30  47350  fourierdlem31  47351  fourierdlem42  47362  fourierdlem47  47366  fourierdlem48  47367  fourierdlem49  47368  fourierdlem63  47382  fourierdlem64  47383  fourierdlem65  47384  fourierdlem71  47390  fourierdlem79  47398  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fouriersw  47444  etransclem28  47475  etransclem48  47495  hoidmv1lelem1  47804  hoidmv1lelem3  47806  hoidmvlelem1  47808  hoidmvlelem4  47811  bgoldbtbndlem2  49107  gpg3kgrtriexlem4  49387  gpg3kgrtriexlem6  49389  lincresunit3lem2  49795  lincresunit3  49796  resum2sqgt0  50022  amgmwlem  51265