Theorem breqtrdi 5141

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breqtrrdi  5142  difsnen  9001  marypha1lem  9350  en2eleq  9932  en2other2  9933  dju0en  10100  pwdju1  10115  pwdjudom  10139  ackbij1lem5  10147  alephadd  10502  prlem934  10958  ltexprlem2  10962  recgt0ii  12062  discr  14177  faclbnd4lem1  14230  hashfun  14374  01sqrexlem7  15185  resqrex  15187  abs3lemi  15348  supcvg  15793  ege2le3  16027  cos01gt0  16130  sin02gt0  16131  bitsfzolem  16375  bitsmod  16377  prmreclem2  16859  f1otrspeq  19393  pmtrf  19401  pmtrmvd  19402  pmtrfinv  19407  efgi0  19666  efgi1  19667  dprdf1  19981  gsumle  20091  metustexhalf  24517  nlmvscnlem2  24646  icccmplem2  24785  xrge0tsms  24796  iimulcl  24906  pcoass  24997  ipcnlem2  25217  ivthlem3  25427  vitalilem4  25585  vitali  25587  dvef  25957  ply1rem  26144  aaliou3lem2  26324  abelthlem8  26422  abelthlem9  26423  cosne0  26511  sinord  26516  tanregt0  26521  argimgt0  26594  logf1o2  26632  logtayllem  26641  cxpcn3lem  26730  ang180lem2  26793  ang180lem3  26794  atanlogsublem  26898  bndatandm  26912  leibpi  26925  emcllem6  26984  emcllem7  26985  lgamgulmlem5  27016  lgamcvg2  27038  ftalem5  27060  basellem7  27070  basellem9  27072  ppieq0  27159  ppiub  27188  chpeq0  27192  chpub  27204  logfacrlim  27208  logexprlim  27209  bposlem1  27268  bposlem2  27269  lgslem3  27283  lgsquadlem1  27364  lgsquadlem3  27366  chebbnd1lem3  27455  chtppilim  27459  chpchtlim  27463  dchrvmasumiflem1  27485  dchrisum0re  27497  mudivsum  27514  mulog2sumlem2  27519  pntibndlem2  27575  pntlemb  27581  pntlemh  27583  ostth3  27622  twocut  28436  addhalfcut  28472  recut  28507  crctcshwlkn0  29912  norm3lem  31243  nmopadjlem  32183  nmopcoadji  32195  hstle  32324  stadd3i  32342  strlem5  32349  pfxlsw2ccat  33049  elrgspnlem1  33342  vietadeg1  33761  locfinreflem  34024  xrge0iifcnv  34117  carsggect  34502  omsmeas  34507  signsply0  34735  signsvtp  34767  tgoldbachgtd  34846  sinccvglem  35894  faclim2  35970  poimirlem28  37928  ismblfin  37941  aks4d1p1p5  42474  sn-0lt1  42874  dffltz  43021  irrapxlem2  43209  pellexlem2  43216  areaquad  43602  dvgrat  44697  binomcxplemrat  44735  fmul01  45969  clim1fr1  45990  sinaover2ne0  46255  stoweidlem14  46401  stoweidlem16  46403  stoweidlem26  46413  stoweidlem41  46428  stoweidlem42  46429  stoweidlem45  46432  wallispi  46457  stirlinglem1  46461  stirlinglem12  46472  fourierdlem24  46518  fourierdlem107  46600  fouriersw  46618  meaiunincf  46870  meaiuninc3  46872  lincfsuppcl  48802  lincresunit3lem2  48869  lincresunit3  48870