Theorem breqtrdi 5148

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breqtrrdi  5149  difsnen  9023  marypha1lem  9384  en2eleq  9961  en2other2  9962  dju0en  10129  pwdju1  10144  pwdjudom  10168  ackbij1lem5  10176  alephadd  10530  prlem934  10986  ltexprlem2  10990  recgt0ii  12089  discr  14205  faclbnd4lem1  14258  hashfun  14402  01sqrexlem7  15214  resqrex  15216  abs3lemi  15377  supcvg  15822  ege2le3  16056  cos01gt0  16159  sin02gt0  16160  bitsfzolem  16404  bitsmod  16406  prmreclem2  16888  f1otrspeq  19377  pmtrf  19385  pmtrmvd  19386  pmtrfinv  19391  efgi0  19650  efgi1  19651  dprdf1  19965  metustexhalf  24444  nlmvscnlem2  24573  icccmplem2  24712  xrge0tsms  24723  iimulcl  24833  pcoass  24924  ipcnlem2  25144  ivthlem3  25354  vitalilem4  25512  vitali  25514  dvef  25884  ply1rem  26071  aaliou3lem2  26251  abelthlem8  26349  abelthlem9  26350  cosne0  26438  sinord  26443  tanregt0  26448  argimgt0  26521  logf1o2  26559  logtayllem  26568  cxpcn3lem  26657  ang180lem2  26720  ang180lem3  26721  atanlogsublem  26825  bndatandm  26839  leibpi  26852  emcllem6  26911  emcllem7  26912  lgamgulmlem5  26943  lgamcvg2  26965  ftalem5  26987  basellem7  26997  basellem9  26999  ppieq0  27086  ppiub  27115  chpeq0  27119  chpub  27131  logfacrlim  27135  logexprlim  27136  bposlem1  27195  bposlem2  27196  lgslem3  27210  lgsquadlem1  27291  lgsquadlem3  27293  chebbnd1lem3  27382  chtppilim  27386  chpchtlim  27390  dchrvmasumiflem1  27412  dchrisum0re  27424  mudivsum  27441  mulog2sumlem2  27446  pntibndlem2  27502  pntlemb  27508  pntlemh  27510  ostth3  27549  twocut  28309  addhalfcut  28334  recut  28347  crctcshwlkn0  29751  norm3lem  31078  nmopadjlem  32018  nmopcoadji  32030  hstle  32159  stadd3i  32177  strlem5  32184  pfxlsw2ccat  32872  gsumle  33038  elrgspnlem1  33193  locfinreflem  33830  xrge0iifcnv  33923  carsggect  34309  omsmeas  34314  signsply0  34542  signsvtp  34574  tgoldbachgtd  34653  sinccvglem  35659  faclim2  35735  poimirlem28  37642  ismblfin  37655  aks4d1p1p5  42063  sn-0lt1  42463  dffltz  42622  irrapxlem2  42811  pellexlem2  42818  areaquad  43205  dvgrat  44301  binomcxplemrat  44339  fmul01  45578  clim1fr1  45599  sinaover2ne0  45866  stoweidlem14  46012  stoweidlem16  46014  stoweidlem26  46024  stoweidlem41  46039  stoweidlem42  46040  stoweidlem45  46043  wallispi  46068  stirlinglem1  46072  stirlinglem12  46083  fourierdlem24  46129  fourierdlem107  46211  fouriersw  46229  meaiunincf  46481  meaiuninc3  46483  lincfsuppcl  48402  lincresunit3lem2  48469  lincresunit3  48470