Theorem breqtrrdi 5134

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  enpr2d  8974  pw2eng  9000  undjudom  10062  dju1en  10066  djucomen  10072  djuassen  10073  xpdjuen  10074  infdjuabs  10099  ackbij1lem9  10121  unsnen  10447  1nqenq  10856  gtndiv  12553  xov1plusxeqvd  13401  intfrac2  13762  serle  13964  discr1  14146  faclbnd4lem1  14200  01sqrexlem1  15149  01sqrexlem4  15152  01sqrexlem7  15155  supcvg  15763  ege2le3  15997  eirrlem  16113  ruclem12  16150  bitsfzo  16346  pcprendvds  16752  pcpremul  16755  pcfaclem  16810  infpnlem2  16823  yonedainv  18187  srgbinomlem4  20114  lmcn2  23534  hmph0  23680  icccmplem2  24710  reconnlem2  24714  xrge0tsms  24721  minveclem2  25324  minveclem3b  25326  minveclem4  25330  minveclem6  25332  ivthlem2  25351  ivthlem3  25352  vitalilem2  25508  itg2seq  25641  itg2monolem1  25649  itg2monolem2  25650  itg2monolem3  25651  dveflem  25881  dvferm1lem  25886  dvferm2lem  25888  c1liplem1  25899  lhop1lem  25916  dvcvx  25923  plyeq0lem  26113  radcnvcl  26324  radcnvle  26327  psercnlem1  26333  psercn  26334  pilem3  26361  tangtx  26412  cos02pilt1  26433  cosne0  26436  recosf1o  26442  resinf1o  26443  efif1olem4  26452  logi  26494  logimul  26521  logcnlem3  26551  logf1o2  26557  ang180lem2  26718  heron  26746  acoscos  26801  emcllem7  26910  fsumharmonic  26920  ftalem2  26982  basellem1  26989  basellem2  26990  basellem3  26991  basellem5  26993  bposlem1  27193  bposlem2  27194  bposlem3  27195  lgsdirprm  27240  chebbnd1lem1  27378  chebbnd1lem2  27379  chebbnd1lem3  27380  mulog2sumlem2  27444  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2  27500  pntlemc  27504  pntlemb  27506  pntlemg  27507  pntlemh  27508  pntlemr  27511  ostth2lem2  27543  ostth2lem3  27544  ostth2lem4  27545  ostth3  27547  axsegconlem3  28868  clwlkclwwlk2  29951  siilem1  30799  minvecolem2  30823  minvecolem4  30828  minvecolem5  30829  minvecolem6  30830  nmopcoi  32043  staddi  32194  cycpmco2lem4  33080  cycpmco2lem5  33081  iconstr  33749  hgt750lemd  34632  climlec3  35727  poimirlem26  37646  ftc1anclem8  37700  cntotbnd  37796  dalemply  39653  dalemsly  39654  dalem5  39666  dalem13  39675  dalem17  39679  dalem55  39726  dalem57  39728  lhpat3  40045  cdleme22aa  40338  aks4d1p1p7  42067  evlselv  42580  jm2.27c  43000  hashnzfz2  44314  supxrubd  45111  suprnmpt  45172  fzisoeu  45302  upbdrech  45307  recnnltrp  45376  uzublem  45429  fmul01  45581  limsupubuzlem  45713  limsupequzmptlem  45729  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  stoweidlem36  46037  stoweidlem41  46042  wallispi2  46074  dirkercncflem1  46104  fourierdlem6  46114  fourierdlem7  46115  fourierdlem19  46127  fourierdlem20  46128  fourierdlem24  46132  fourierdlem25  46133  fourierdlem26  46134  fourierdlem30  46138  fourierdlem31  46139  fourierdlem42  46150  fourierdlem47  46154  fourierdlem48  46155  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem71  46178  fourierdlem79  46186  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fouriersw  46232  etransclem28  46263  etransclem48  46283  hoidmv1lelem1  46592  hoidmv1lelem3  46594  hoidmvlelem1  46596  hoidmvlelem4  46599  bgoldbtbndlem2  47810  gpg3kgrtriexlem4  48090  gpg3kgrtriexlem6  48092  lincresunit3lem2  48485  lincresunit3  48486  resum2sqgt0  48712  amgmwlem  49807