Theorem breqtrdi 5150

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breqtrrdi  5151  difsnen  9060  marypha1lem  9406  en2eleq  10014  en2other2  10015  dju0en  10181  pwdju1  10196  pwdjudom  10220  ackbij1lem5  10228  alephadd  10589  prlem934  11045  ltexprlem2  11049  recgt0ii  12148  discr  14306  faclbnd4lem1  14359  hashfun  14504  01sqrexlem7  15337  resqrex  15339  abs3lemi  15500  supcvg  15947  ege2le3  16180  cos01gt0  16283  sin02gt0  16284  bitsfzolem  16528  bitsmod  16530  prmreclem2  17013  f1otrspeq  19575  pmtrf  19583  pmtrmvd  19584  pmtrfinv  19589  efgi0  19848  efgi1  19849  dprdf1  20163  gsumle  20273  metustexhalf  24783  nlmvscnlem2  24912  icccmplem2  25051  xrge0tsms  25062  iimulcl  25166  pcoass  25253  ipcnlem2  25473  ivthlem3  25682  vitalilem4  25840  vitali  25842  dvef  26209  ply1rem  26393  aaliou3lem2  26576  abelthlem8  26672  abelthlem9  26673  cosne0  26764  sinord  26769  tanregt0  26774  argimgt0  26847  logf1o2  26885  logtayllem  26894  cxpcn3lem  26982  ang180lem2  27045  ang180lem3  27046  atanlogsublem  27150  bndatandm  27164  leibpi  27177  emcllem6  27235  emcllem7  27236  lgamgulmlem5  27267  lgamcvg2  27289  ftalem5  27311  basellem7  27321  basellem9  27323  ppieq0  27410  ppiub  27438  chpeq0  27442  chpub  27454  logfacrlim  27458  logexprlim  27459  bposlem1  27518  bposlem2  27519  lgslem3  27533  lgsquadlem1  27614  lgsquadlem3  27616  chebbnd1lem3  27705  chtppilim  27709  chpchtlim  27713  dchrvmasumiflem1  27735  dchrisum0re  27747  mudivsum  27764  mulog2sumlem2  27769  pntibndlem2  27825  pntlemb  27831  pntlemh  27833  ostth3  27872  twocut  28686  addhalfcut  28722  recut  28757  crctcshwlkn0  30275  norm3lem  31616  nmopadjlem  32556  nmopcoadji  32568  hstle  32697  stadd3i  32715  strlem5  32722  pfxlsw2ccat  33379  elrgspnlem1  33669  vietadeg1  34075  locfinreflem  34337  xrge0iifcnv  34430  carsggect  34816  omsmeas  34821  signsply0  35046  signsvtp  35078  tgoldbachgtd  35157  1enumen  35586  sinccvglem  36238  faclim2  36314  poimirlem28  38384  ismblfin  38397  aks4d1p1p5  42928  sn-0lt1  43350  dffltz  43467  irrapxlem2  43651  pellexlem2  43658  areaquad  44044  dvgrat  45123  binomcxplemrat  45161  fmul01  46397  clim1fr1  46418  sinaover2ne0  46683  stoweidlem14  46829  stoweidlem16  46831  stoweidlem26  46841  stoweidlem41  46856  stoweidlem42  46857  stoweidlem45  46860  wallispi  46885  stirlinglem1  46889  stirlinglem12  46900  fourierdlem24  46946  fourierdlem107  47028  fouriersw  47046  meaiunincf  47298  meaiuninc3  47300  lincfsuppcl  49330  lincresunit3lem2  49397  lincresunit3  49398