Theorem breqtrrdi 5146

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 5145	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  enpr2d  9076  pw2eng  9102  undjudom  10246  dju1en  10250  djucomen  10256  djuassen  10257  xpdjuen  10258  infdjuabs  10283  ackbij1lem9  10305  unsnen  10637  1nqenq  11047  gtndiv  12776  xov1plusxeqvd  13629  intfrac2  13998  serle  14200  discr1  14383  faclbnd4lem1  14437  01sqrexlem1  15409  01sqrexlem4  15412  01sqrexlem7  15415  supcvg  16025  ege2le3  16256  eirrlem  16372  ruclem12  16409  bitsfzo  16605  pcprendvds  17018  pcpremul  17021  pcfaclem  17076  infpnlem2  17089  yonedainv  18455  srgbinomlem4  20455  lmcn2  23968  hmph0  24114  icccmplem2  25143  reconnlem2  25147  xrge0tsms  25154  minveclem2  25747  minveclem3b  25749  minveclem4  25753  minveclem6  25755  ivthlem2  25773  ivthlem3  25774  vitalilem2  25930  itg2seq  26063  itg2monolem1  26071  itg2monolem2  26072  itg2monolem3  26073  dveflem  26299  dvferm1lem  26304  dvferm2lem  26306  c1liplem1  26316  lhop1lem  26333  dvcvx  26340  plyeq0lem  26529  radcnvcl  26744  radcnvle  26747  psercnlem1  26752  psercn  26753  pilem3  26780  tangtx  26834  cos02pilt1  26854  cosne0  26857  recosf1o  26863  resinf1o  26864  efif1olem4  26873  logi  26915  logimul  26942  logcnlem3  26972  logf1o2  26978  ang180lem2  27138  heron  27166  acoscos  27221  emcllem7  27329  fsumharmonic  27339  ftalem2  27401  basellem1  27408  basellem2  27409  basellem3  27410  basellem5  27412  bposlem1  27611  bposlem2  27612  bposlem3  27613  lgsdirprm  27658  chebbnd1lem1  27796  chebbnd1lem2  27797  chebbnd1lem3  27798  mulog2sumlem2  27862  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2  27918  pntlemc  27922  pntlemb  27924  pntlemg  27925  pntlemh  27926  pntlemr  27929  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ostth3  27965  axsegconlem3  29497  clwlkclwwlk2  30594  siilem1  31453  minvecolem2  31477  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  nmopcoi  32697  staddi  32848  cycpmco2lem4  33690  cycpmco2lem5  33691  iconstr  34398  hgt750lemd  35277  climlec3  36499  poimirlem26  38565  ftc1anclem8  38619  cntotbnd  38731  dalemply  40712  dalemsly  40713  dalem5  40725  dalem13  40734  dalem17  40738  dalem55  40785  dalem57  40787  lhpat3  41104  cdleme22aa  41397  aks4d1p1p7  43125  evlselv  43618  jm2.27c  44014  hashnzfz2  45305  supxrubd  46128  suprnmpt  46189  fzisoeu  46316  upbdrech  46321  recnnltrp  46388  uzublem  46440  fmul01  46592  limsupubuzlem  46722  limsupequzmptlem  46738  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  stoweidlem36  47046  stoweidlem41  47051  wallispi2  47083  dirkercncflem1  47113  fourierdlem6  47123  fourierdlem7  47124  fourierdlem19  47136  fourierdlem20  47137  fourierdlem24  47141  fourierdlem25  47142  fourierdlem26  47143  fourierdlem30  47147  fourierdlem31  47148  fourierdlem42  47159  fourierdlem47  47163  fourierdlem48  47164  fourierdlem49  47165  fourierdlem63  47179  fourierdlem64  47180  fourierdlem65  47181  fourierdlem71  47187  fourierdlem79  47195  fourierdlem89  47205  fourierdlem90  47206  fourierdlem91  47207  fouriersw  47241  etransclem28  47272  etransclem48  47292  hoidmv1lelem1  47601  hoidmv1lelem3  47603  hoidmvlelem1  47605  hoidmvlelem4  47608  bgoldbtbndlem2  48904  gpg3kgrtriexlem4  49184  gpg3kgrtriexlem6  49186  lincresunit3lem2  49592  lincresunit3  49593  resum2sqgt0  49819  amgmwlem  50987