Theorem breqtrdi 5143

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 5135	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtrrdi  5144  difsnen  9000  marypha1lem  9360  en2eleq  9937  en2other2  9938  dju0en  10105  pwdju1  10120  pwdjudom  10144  ackbij1lem5  10152  alephadd  10506  prlem934  10962  ltexprlem2  10966  recgt0ii  12065  discr  14181  faclbnd4lem1  14234  hashfun  14378  01sqrexlem7  15190  resqrex  15192  abs3lemi  15353  supcvg  15798  ege2le3  16032  cos01gt0  16135  sin02gt0  16136  bitsfzolem  16380  bitsmod  16382  prmreclem2  16864  f1otrspeq  19361  pmtrf  19369  pmtrmvd  19370  pmtrfinv  19375  efgi0  19634  efgi1  19635  dprdf1  19949  gsumle  20059  metustexhalf  24477  nlmvscnlem2  24606  icccmplem2  24745  xrge0tsms  24756  iimulcl  24866  pcoass  24957  ipcnlem2  25177  ivthlem3  25387  vitalilem4  25545  vitali  25547  dvef  25917  ply1rem  26104  aaliou3lem2  26284  abelthlem8  26382  abelthlem9  26383  cosne0  26471  sinord  26476  tanregt0  26481  argimgt0  26554  logf1o2  26592  logtayllem  26601  cxpcn3lem  26690  ang180lem2  26753  ang180lem3  26754  atanlogsublem  26858  bndatandm  26872  leibpi  26885  emcllem6  26944  emcllem7  26945  lgamgulmlem5  26976  lgamcvg2  26998  ftalem5  27020  basellem7  27030  basellem9  27032  ppieq0  27119  ppiub  27148  chpeq0  27152  chpub  27164  logfacrlim  27168  logexprlim  27169  bposlem1  27228  bposlem2  27229  lgslem3  27243  lgsquadlem1  27324  lgsquadlem3  27326  chebbnd1lem3  27415  chtppilim  27419  chpchtlim  27423  dchrvmasumiflem1  27445  dchrisum0re  27457  mudivsum  27474  mulog2sumlem2  27479  pntibndlem2  27535  pntlemb  27541  pntlemh  27543  ostth3  27582  twocut  28350  addhalfcut  28382  recut  28400  crctcshwlkn0  29801  norm3lem  31128  nmopadjlem  32068  nmopcoadji  32080  hstle  32209  stadd3i  32227  strlem5  32234  pfxlsw2ccat  32922  elrgspnlem1  33209  locfinreflem  33823  xrge0iifcnv  33916  carsggect  34302  omsmeas  34307  signsply0  34535  signsvtp  34567  tgoldbachgtd  34646  sinccvglem  35652  faclim2  35728  poimirlem28  37635  ismblfin  37648  aks4d1p1p5  42056  sn-0lt1  42456  dffltz  42615  irrapxlem2  42804  pellexlem2  42811  areaquad  43198  dvgrat  44294  binomcxplemrat  44332  fmul01  45571  clim1fr1  45592  sinaover2ne0  45859  stoweidlem14  46005  stoweidlem16  46007  stoweidlem26  46017  stoweidlem41  46032  stoweidlem42  46033  stoweidlem45  46036  wallispi  46061  stirlinglem1  46065  stirlinglem12  46076  fourierdlem24  46122  fourierdlem107  46204  fouriersw  46222  meaiunincf  46474  meaiuninc3  46476  lincfsuppcl  48395  lincresunit3lem2  48462  lincresunit3  48463