Theorem breqtrrdi 5152

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  enpr2d  9023  enpr2dOLD  9024  pw2eng  9052  undjudom  10128  dju1en  10132  djucomen  10138  djuassen  10139  xpdjuen  10140  infdjuabs  10165  ackbij1lem9  10187  unsnen  10513  1nqenq  10922  gtndiv  12618  xov1plusxeqvd  13466  intfrac2  13827  serle  14029  discr1  14211  faclbnd4lem1  14265  01sqrexlem1  15215  01sqrexlem4  15218  01sqrexlem7  15221  supcvg  15829  ege2le3  16063  eirrlem  16179  ruclem12  16216  bitsfzo  16412  pcprendvds  16818  pcpremul  16821  pcfaclem  16876  infpnlem2  16889  yonedainv  18249  srgbinomlem4  20145  lmcn2  23543  hmph0  23689  icccmplem2  24719  reconnlem2  24723  xrge0tsms  24730  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  ivthlem2  25360  ivthlem3  25361  vitalilem2  25517  itg2seq  25650  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  dveflem  25890  dvferm1lem  25895  dvferm2lem  25897  c1liplem1  25908  lhop1lem  25925  dvcvx  25932  plyeq0lem  26122  radcnvcl  26333  radcnvle  26336  psercnlem1  26342  psercn  26343  pilem3  26370  tangtx  26421  cos02pilt1  26442  cosne0  26445  recosf1o  26451  resinf1o  26452  efif1olem4  26461  logi  26503  logimul  26530  logcnlem3  26560  logf1o2  26566  ang180lem2  26727  heron  26755  acoscos  26810  emcllem7  26919  fsumharmonic  26929  ftalem2  26991  basellem1  26998  basellem2  26999  basellem3  27000  basellem5  27002  bposlem1  27202  bposlem2  27203  bposlem3  27204  lgsdirprm  27249  chebbnd1lem1  27387  chebbnd1lem2  27388  chebbnd1lem3  27389  mulog2sumlem2  27453  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2  27509  pntlemc  27513  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemr  27520  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth3  27556  axsegconlem3  28853  clwlkclwwlk2  29939  siilem1  30787  minvecolem2  30811  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  nmopcoi  32031  staddi  32182  cycpmco2lem4  33093  cycpmco2lem5  33094  iconstr  33763  hgt750lemd  34646  climlec3  35728  poimirlem26  37647  ftc1anclem8  37701  cntotbnd  37797  dalemply  39655  dalemsly  39656  dalem5  39668  dalem13  39677  dalem17  39681  dalem55  39728  dalem57  39730  lhpat3  40047  cdleme22aa  40340  aks4d1p1p7  42069  evlselv  42582  jm2.27c  43003  hashnzfz2  44317  supxrubd  45114  suprnmpt  45175  fzisoeu  45305  upbdrech  45310  recnnltrp  45380  uzublem  45433  fmul01  45585  limsupubuzlem  45717  limsupequzmptlem  45733  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem36  46041  stoweidlem41  46046  wallispi2  46078  dirkercncflem1  46108  fourierdlem6  46118  fourierdlem7  46119  fourierdlem19  46131  fourierdlem20  46132  fourierdlem24  46136  fourierdlem25  46137  fourierdlem26  46138  fourierdlem30  46142  fourierdlem31  46143  fourierdlem42  46154  fourierdlem47  46158  fourierdlem48  46159  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem71  46182  fourierdlem79  46190  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fouriersw  46236  etransclem28  46267  etransclem48  46287  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem4  46603  bgoldbtbndlem2  47811  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  lincresunit3lem2  48473  lincresunit3  48474  resum2sqgt0  48700  amgmwlem  49795