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

Syntax hints:   → wi 4   = wceq 1539   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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  breqtrrdi  5117  difsnen  8849  marypha1lem  9201  en2eleq  9773  en2other2  9774  dju0en  9940  pwdju1  9955  pwdjudom  9981  ackbij1lem5  9989  alephadd  10342  prlem934  10798  ltexprlem2  10802  recgt0ii  11890  discr  13964  faclbnd4lem1  14016  hashfun  14161  sqrlem7  14969  resqrex  14971  abs3lemi  15131  supcvg  15577  ege2le3  15808  cos01gt0  15909  sin02gt0  15910  bitsfzolem  16150  bitsmod  16152  prmreclem2  16627  f1otrspeq  19064  pmtrf  19072  pmtrmvd  19073  pmtrfinv  19078  efgi0  19335  efgi1  19336  dprdf1  19645  metustexhalf  23721  nlmvscnlem2  23858  icccmplem2  23995  xrge0tsms  24006  iimulcl  24109  pcoass  24196  ipcnlem2  24417  ivthlem3  24626  vitalilem4  24784  vitali  24786  dvef  25153  ply1rem  25337  aaliou3lem2  25512  abelthlem8  25607  abelthlem9  25608  cosne0  25694  sinord  25699  tanregt0  25704  argimgt0  25776  logf1o2  25814  logtayllem  25823  cxpcn3lem  25909  ang180lem2  25969  ang180lem3  25970  atanlogsublem  26074  bndatandm  26088  leibpi  26101  emcllem6  26159  emcllem7  26160  lgamgulmlem5  26191  lgamcvg2  26213  ftalem5  26235  basellem7  26245  basellem9  26247  ppieq0  26334  ppiub  26361  chpeq0  26365  chpub  26377  logfacrlim  26381  logexprlim  26382  bposlem1  26441  bposlem2  26442  lgslem3  26456  lgsquadlem1  26537  lgsquadlem3  26539  chebbnd1lem3  26628  chtppilim  26632  chpchtlim  26636  dchrvmasumiflem1  26658  dchrisum0re  26670  mudivsum  26687  mulog2sumlem2  26692  pntibndlem2  26748  pntlemb  26754  pntlemh  26756  ostth3  26795  crctcshwlkn0  28195  norm3lem  29520  nmopadjlem  30460  nmopcoadji  30472  hstle  30601  stadd3i  30619  strlem5  30626  pfxlsw2ccat  31233  gsumle  31359  locfinreflem  31799  xrge0iifcnv  31892  carsggect  32294  omsmeas  32299  signsply0  32539  signsvtp  32571  tgoldbachgtd  32651  sinccvglem  33639  faclim2  33723  poimirlem28  35814  ismblfin  35827  aks4d1p1p5  40090  sn-0lt1  40439  sn-inelr  40442  dffltz  40478  irrapxlem2  40652  pellexlem2  40659  areaquad  41054  dvgrat  41937  binomcxplemrat  41975  fmul01  43128  clim1fr1  43149  sinaover2ne0  43416  stoweidlem14  43562  stoweidlem16  43564  stoweidlem26  43574  stoweidlem41  43589  stoweidlem42  43590  stoweidlem45  43593  wallispi  43618  stirlinglem1  43622  stirlinglem12  43633  fourierdlem24  43679  fourierdlem107  43761  fouriersw  43779  meaiunincf  44028  meaiuninc3  44030  lincfsuppcl  45765  lincresunit3lem2  45832  lincresunit3  45833