Theorem breqtrdi 5116

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  breqtrrdi  5117  difsnen  8991  marypha1lem  9340  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  24543  nlmvscnlem2  24672  icccmplem2  24811  xrge0tsms  24822  iimulcl  24926  pcoass  25013  ipcnlem2  25233  ivthlem3  25442  vitalilem4  25600  vitali  25602  dvef  25969  ply1rem  26153  aaliou3lem2  26331  abelthlem8  26426  abelthlem9  26427  cosne0  26515  sinord  26520  tanregt0  26525  argimgt0  26598  logf1o2  26636  logtayllem  26645  cxpcn3lem  26733  ang180lem2  26796  ang180lem3  26797  atanlogsublem  26901  bndatandm  26915  leibpi  26928  emcllem6  26986  emcllem7  26987  lgamgulmlem5  27018  lgamcvg2  27040  ftalem5  27062  basellem7  27072  basellem9  27074  ppieq0  27161  ppiub  27189  chpeq0  27193  chpub  27205  logfacrlim  27209  logexprlim  27210  bposlem1  27269  bposlem2  27270  lgslem3  27284  lgsquadlem1  27365  lgsquadlem3  27367  chebbnd1lem3  27456  chtppilim  27460  chpchtlim  27464  dchrvmasumiflem1  27486  dchrisum0re  27498  mudivsum  27515  mulog2sumlem2  27520  pntibndlem2  27576  pntlemb  27582  pntlemh  27584  ostth3  27623  twocut  28437  addhalfcut  28473  recut  28508  crctcshwlkn0  29911  norm3lem  31242  nmopadjlem  32182  nmopcoadji  32194  hstle  32323  stadd3i  32341  strlem5  32348  pfxlsw2ccat  33033  elrgspnlem1  33327  vietadeg1  33774  locfinreflem  34036  xrge0iifcnv  34129  carsggect  34514  omsmeas  34519  signsply0  34747  signsvtp  34779  tgoldbachgtd  34858  sinccvglem  35915  faclim2  35991  poimirlem28  38030  ismblfin  38043  aks4d1p1p5  42575  sn-0lt1  42980  dffltz  43099  irrapxlem2  43283  pellexlem2  43290  areaquad  43676  dvgrat  44771  binomcxplemrat  44809  fmul01  46039  clim1fr1  46060  sinaover2ne0  46325  stoweidlem14  46471  stoweidlem16  46473  stoweidlem26  46483  stoweidlem41  46498  stoweidlem42  46499  stoweidlem45  46502  wallispi  46527  stirlinglem1  46531  stirlinglem12  46542  fourierdlem24  46588  fourierdlem107  46670  fouriersw  46688  meaiunincf  46940  meaiuninc3  46942  lincfsuppcl  48918  lincresunit3lem2  48985  lincresunit3  48986