Theorem breqtrdi 5146

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqtrrdi  5147  difsnen  9057  marypha1lem  9403  en2eleq  10044  en2other2  10045  dju0en  10211  pwdju1  10226  pwdjudom  10250  ackbij1lem5  10258  alephadd  10619  prlem934  11075  ltexprlem2  11079  recgt0ii  12178  discr  14337  faclbnd4lem1  14390  hashfun  14535  01sqrexlem7  15368  resqrex  15370  abs3lemi  15531  supcvg  15978  ege2le3  16209  cos01gt0  16312  sin02gt0  16313  bitsfzolem  16557  bitsmod  16559  prmreclem2  17042  f1otrspeq  19608  pmtrf  19616  pmtrmvd  19617  pmtrfinv  19622  efgi0  19881  efgi1  19882  dprdf1  20196  gsumle  20306  metustexhalf  24822  nlmvscnlem2  24951  icccmplem2  25090  xrge0tsms  25101  iimulcl  25205  pcoass  25292  ipcnlem2  25512  ivthlem3  25721  vitalilem4  25879  vitali  25881  dvef  26247  ply1rem  26431  aaliou3lem2  26619  abelthlem8  26715  abelthlem9  26716  cosne0  26806  sinord  26811  tanregt0  26816  argimgt0  26889  logf1o2  26927  logtayllem  26936  cxpcn3lem  27024  ang180lem2  27087  ang180lem3  27088  atanlogsublem  27192  bndatandm  27206  leibpi  27219  emcllem6  27277  emcllem7  27278  lgamgulmlem5  27309  lgamcvg2  27331  ftalem5  27353  basellem7  27363  basellem9  27365  ppieq0  27452  ppiub  27480  chpeq0  27484  chpub  27496  logfacrlim  27500  logexprlim  27501  bposlem1  27560  bposlem2  27561  lgslem3  27575  lgsquadlem1  27656  lgsquadlem3  27658  chebbnd1lem3  27747  chtppilim  27751  chpchtlim  27755  dchrvmasumiflem1  27777  dchrisum0re  27789  mudivsum  27806  mulog2sumlem2  27811  pntibndlem2  27867  pntlemb  27873  pntlemh  27875  ostth3  27914  twocut  28728  addhalfcut  28764  recut  28799  crctcshwlkn0  30329  norm3lem  31670  nmopadjlem  32610  nmopcoadji  32622  hstle  32751  stadd3i  32769  strlem5  32776  pfxlsw2ccat  33432  elrgspnlem1  33722  vietadeg1  34129  locfinreflem  34391  xrge0iifcnv  34484  carsggect  34870  omsmeas  34875  signsply0  35100  signsvtp  35132  tgoldbachgtd  35211  1enumen  35640  sinccvglem  36352  faclim2  36428  poimirlem28  38480  ismblfin  38493  aks4d1p1p5  43039  sn-0lt1  43461  dffltz  43578  irrapxlem2  43762  pellexlem2  43769  areaquad  44155  dvgrat  45234  binomcxplemrat  45272  fmul01  46508  clim1fr1  46529  sinaover2ne0  46794  stoweidlem14  46940  stoweidlem16  46942  stoweidlem26  46952  stoweidlem41  46967  stoweidlem42  46968  stoweidlem45  46971  wallispi  46996  stirlinglem1  47000  stirlinglem12  47011  fourierdlem24  47057  fourierdlem107  47139  fouriersw  47157  meaiunincf  47409  meaiuninc3  47411  lincfsuppcl  49441  lincresunit3lem2  49508  lincresunit3  49509