Theorem breqtrdi 5166

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
breqtrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrdi.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
breqtrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrdi

Step	Hyp	Ref	Expression
1		breqtrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		eqid 2734	. 2 ⊢ 𝐴 = 𝐴
3		breqtrdi.2	. 2 ⊢ 𝐵 = 𝐶
4	1, 2, 3	3brtr3g 5158	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126

This theorem is referenced by:  breqtrrdi  5167  difsnen  9076  marypha1lem  9456  en2eleq  10031  en2other2  10032  dju0en  10199  pwdju1  10214  pwdjudom  10238  ackbij1lem5  10246  alephadd  10600  prlem934  11056  ltexprlem2  11060  recgt0ii  12157  discr  14262  faclbnd4lem1  14315  hashfun  14459  01sqrexlem7  15270  resqrex  15272  abs3lemi  15432  supcvg  15875  ege2le3  16109  cos01gt0  16210  sin02gt0  16211  bitsfzolem  16454  bitsmod  16456  prmreclem2  16938  f1otrspeq  19438  pmtrf  19446  pmtrmvd  19447  pmtrfinv  19452  efgi0  19711  efgi1  19712  dprdf1  20026  metustexhalf  24532  nlmvscnlem2  24661  icccmplem2  24800  xrge0tsms  24811  iimulcl  24921  pcoass  25012  ipcnlem2  25233  ivthlem3  25443  vitalilem4  25601  vitali  25603  dvef  25973  ply1rem  26160  aaliou3lem2  26340  abelthlem8  26438  abelthlem9  26439  cosne0  26526  sinord  26531  tanregt0  26536  argimgt0  26609  logf1o2  26647  logtayllem  26656  cxpcn3lem  26745  ang180lem2  26808  ang180lem3  26809  atanlogsublem  26913  bndatandm  26927  leibpi  26940  emcllem6  26999  emcllem7  27000  lgamgulmlem5  27031  lgamcvg2  27053  ftalem5  27075  basellem7  27085  basellem9  27087  ppieq0  27174  ppiub  27203  chpeq0  27207  chpub  27219  logfacrlim  27223  logexprlim  27224  bposlem1  27283  bposlem2  27284  lgslem3  27298  lgsquadlem1  27379  lgsquadlem3  27381  chebbnd1lem3  27470  chtppilim  27474  chpchtlim  27478  dchrvmasumiflem1  27500  dchrisum0re  27512  mudivsum  27529  mulog2sumlem2  27534  pntibndlem2  27590  pntlemb  27596  pntlemh  27598  ostth3  27637  addhalfcut  28374  recut  28383  crctcshwlkn0  29788  norm3lem  31115  nmopadjlem  32055  nmopcoadji  32067  hstle  32196  stadd3i  32214  strlem5  32221  pfxlsw2ccat  32882  gsumle  33047  elrgspnlem1  33192  locfinreflem  33780  xrge0iifcnv  33873  carsggect  34261  omsmeas  34266  signsply0  34507  signsvtp  34539  tgoldbachgtd  34618  sinccvglem  35618  faclim2  35689  poimirlem28  37596  ismblfin  37609  aks4d1p1p5  42017  sn-0lt1  42438  sn-inelr  42442  dffltz  42589  irrapxlem2  42779  pellexlem2  42786  areaquad  43173  dvgrat  44276  binomcxplemrat  44314  fmul01  45540  clim1fr1  45561  sinaover2ne0  45828  stoweidlem14  45974  stoweidlem16  45976  stoweidlem26  45986  stoweidlem41  46001  stoweidlem42  46002  stoweidlem45  46005  wallispi  46030  stirlinglem1  46034  stirlinglem12  46045  fourierdlem24  46091  fourierdlem107  46173  fouriersw  46191  meaiunincf  46443  meaiuninc3  46445  lincfsuppcl  48276  lincresunit3lem2  48343  lincresunit3  48344