Theorem breqtrdi 5127

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breqtrrdi  5128  difsnen  8992  marypha1lem  9341  en2eleq  9925  en2other2  9926  dju0en  10093  pwdju1  10108  pwdjudom  10132  ackbij1lem5  10140  alephadd  10495  prlem934  10951  ltexprlem2  10955  recgt0ii  12057  discr  14197  faclbnd4lem1  14250  hashfun  14394  01sqrexlem7  15205  resqrex  15207  abs3lemi  15368  supcvg  15816  ege2le3  16050  cos01gt0  16153  sin02gt0  16154  bitsfzolem  16398  bitsmod  16400  prmreclem2  16883  f1otrspeq  19417  pmtrf  19425  pmtrmvd  19426  pmtrfinv  19431  efgi0  19690  efgi1  19691  dprdf1  20005  gsumle  20115  metustexhalf  24535  nlmvscnlem2  24664  icccmplem2  24803  xrge0tsms  24814  iimulcl  24918  pcoass  25005  ipcnlem2  25225  ivthlem3  25434  vitalilem4  25592  vitali  25594  dvef  25961  ply1rem  26145  aaliou3lem2  26324  abelthlem8  26421  abelthlem9  26422  cosne0  26510  sinord  26515  tanregt0  26520  argimgt0  26593  logf1o2  26631  logtayllem  26640  cxpcn3lem  26728  ang180lem2  26791  ang180lem3  26792  atanlogsublem  26896  bndatandm  26910  leibpi  26923  emcllem6  26982  emcllem7  26983  lgamgulmlem5  27014  lgamcvg2  27036  ftalem5  27058  basellem7  27068  basellem9  27070  ppieq0  27157  ppiub  27185  chpeq0  27189  chpub  27201  logfacrlim  27205  logexprlim  27206  bposlem1  27265  bposlem2  27266  lgslem3  27280  lgsquadlem1  27361  lgsquadlem3  27363  chebbnd1lem3  27452  chtppilim  27456  chpchtlim  27460  dchrvmasumiflem1  27482  dchrisum0re  27494  mudivsum  27511  mulog2sumlem2  27516  pntibndlem2  27572  pntlemb  27578  pntlemh  27580  ostth3  27619  twocut  28433  addhalfcut  28469  recut  28504  crctcshwlkn0  29908  norm3lem  31239  nmopadjlem  32179  nmopcoadji  32191  hstle  32320  stadd3i  32338  strlem5  32345  pfxlsw2ccat  33029  elrgspnlem1  33322  vietadeg1  33741  locfinreflem  34004  xrge0iifcnv  34097  carsggect  34482  omsmeas  34487  signsply0  34715  signsvtp  34747  tgoldbachgtd  34826  sinccvglem  35874  faclim2  35950  poimirlem28  37989  ismblfin  38002  aks4d1p1p5  42534  sn-0lt1  42940  dffltz  43087  irrapxlem2  43275  pellexlem2  43282  areaquad  43668  dvgrat  44763  binomcxplemrat  44801  fmul01  46034  clim1fr1  46055  sinaover2ne0  46320  stoweidlem14  46466  stoweidlem16  46468  stoweidlem26  46478  stoweidlem41  46493  stoweidlem42  46494  stoweidlem45  46497  wallispi  46522  stirlinglem1  46526  stirlinglem12  46537  fourierdlem24  46583  fourierdlem107  46665  fouriersw  46683  meaiunincf  46935  meaiuninc3  46937  lincfsuppcl  48907  lincresunit3lem2  48974  lincresunit3  48975