Theorem breqtrrdi 5144

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

Syntax hints:   → wi 4   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  enpr2d  9031  pw2eng  9057  undjudom  10126  dju1en  10130  djucomen  10136  djuassen  10137  xpdjuen  10138  infdjuabs  10163  ackbij1lem9  10185  unsnen  10512  1nqenq  10922  gtndiv  12652  xov1plusxeqvd  13504  intfrac2  13870  serle  14072  discr1  14254  faclbnd4lem1  14308  01sqrexlem1  15271  01sqrexlem4  15274  01sqrexlem7  15277  supcvg  15888  ege2le3  16122  eirrlem  16238  ruclem12  16275  bitsfzo  16471  pcprendvds  16878  pcpremul  16881  pcfaclem  16936  infpnlem2  16949  yonedainv  18315  srgbinomlem4  20281  lmcn2  23711  hmph0  23857  icccmplem2  24886  reconnlem2  24890  xrge0tsms  24897  minveclem2  25490  minveclem3b  25492  minveclem4  25496  minveclem6  25498  ivthlem2  25516  ivthlem3  25517  vitalilem2  25673  itg2seq  25806  itg2monolem1  25814  itg2monolem2  25815  itg2monolem3  25816  dveflem  26043  dvferm1lem  26048  dvferm2lem  26050  c1liplem1  26060  lhop1lem  26077  dvcvx  26084  plyeq0lem  26272  radcnvcl  26482  radcnvle  26485  psercnlem1  26490  psercn  26491  pilem3  26518  tangtx  26572  cos02pilt1  26593  cosne0  26596  recosf1o  26602  resinf1o  26603  efif1olem4  26612  logi  26654  logimul  26681  logcnlem3  26711  logf1o2  26717  ang180lem2  26877  heron  26905  acoscos  26960  emcllem7  27068  fsumharmonic  27078  ftalem2  27140  basellem1  27147  basellem2  27148  basellem3  27149  basellem5  27151  bposlem1  27350  bposlem2  27351  bposlem3  27352  lgsdirprm  27397  chebbnd1lem1  27535  chebbnd1lem2  27536  chebbnd1lem3  27537  mulog2sumlem2  27601  pntpbnd1a  27651  pntpbnd1  27652  pntpbnd2  27653  pntibndlem2  27657  pntlemc  27661  pntlemb  27663  pntlemg  27664  pntlemh  27665  pntlemr  27668  ostth2lem2  27700  ostth2lem3  27701  ostth2lem4  27702  ostth3  27704  axsegconlem3  29122  clwlkclwwlk2  30207  siilem1  31056  minvecolem2  31080  minvecolem4  31085  minvecolem5  31086  minvecolem6  31087  nmopcoi  32300  staddi  32451  cycpmco2lem4  33311  cycpmco2lem5  33312  iconstr  34065  hgt750lemd  34944  climlec3  36089  poimirlem26  38150  ftc1anclem8  38204  cntotbnd  38300  dalemply  40283  dalemsly  40284  dalem5  40296  dalem13  40305  dalem17  40309  dalem55  40356  dalem57  40358  lhpat3  40675  cdleme22aa  40968  aks4d1p1p7  42696  evlselv  43176  jm2.27c  43589  hashnzfz2  44902  supxrubd  45696  suprnmpt  45757  fzisoeu  45884  upbdrech  45889  recnnltrp  45957  uzublem  46009  fmul01  46161  limsupubuzlem  46291  limsupequzmptlem  46307  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweidlem36  46615  stoweidlem41  46620  wallispi2  46652  dirkercncflem1  46682  fourierdlem6  46692  fourierdlem7  46693  fourierdlem19  46705  fourierdlem20  46706  fourierdlem24  46710  fourierdlem25  46711  fourierdlem26  46712  fourierdlem30  46716  fourierdlem31  46717  fourierdlem42  46728  fourierdlem47  46732  fourierdlem48  46733  fourierdlem49  46734  fourierdlem63  46748  fourierdlem64  46749  fourierdlem65  46750  fourierdlem71  46756  fourierdlem79  46764  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fouriersw  46810  etransclem28  46841  etransclem48  46861  hoidmv1lelem1  47170  hoidmv1lelem3  47172  hoidmvlelem1  47174  hoidmvlelem4  47177  bgoldbtbndlem2  48433  gpg3kgrtriexlem4  48713  gpg3kgrtriexlem6  48715  lincresunit3lem2  49107  lincresunit3  49108  resum2sqgt0  49334  amgmwlem  50428