Theorem breqtrdi 5149

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breqtrrdi  5150  difsnen  9103  marypha1lem  9449  en2eleq  10111  en2other2  10112  dju0en  10278  pwdju1  10293  pwdjudom  10317  ackbij1lem5  10325  alephadd  10686  prlem934  11142  ltexprlem2  11146  recgt0ii  12247  discr  14408  faclbnd4lem1  14461  hashfun  14606  01sqrexlem7  15441  resqrex  15443  abs3lemi  15604  supcvg  16051  ege2le3  16282  cos01gt0  16385  sin02gt0  16386  bitsfzolem  16630  bitsmod  16632  prmreclem2  17121  f1otrspeq  19688  pmtrf  19696  pmtrmvd  19697  pmtrfinv  19702  efgi0  19961  efgi1  19962  dprdf1  20276  gsumle  20386  metustexhalf  24902  nlmvscnlem2  25031  icccmplem2  25170  xrge0tsms  25181  iimulcl  25285  pcoass  25372  ipcnlem2  25592  ivthlem3  25801  vitalilem4  25959  vitali  25961  dvef  26327  ply1rem  26511  aaliou3lem2  26697  abelthlem8  26793  abelthlem9  26794  cosne0  26884  sinord  26889  tanregt0  26894  argimgt0  26967  logf1o2  27005  logtayllem  27014  cxpcn3lem  27102  ang180lem2  27165  ang180lem3  27166  atanlogsublem  27270  bndatandm  27284  leibpi  27297  emcllem6  27355  emcllem7  27356  lgamgulmlem5  27387  lgamcvg2  27409  ftalem5  27431  basellem7  27441  basellem9  27443  ppieq0  27530  ppiub  27558  chpeq0  27562  chpub  27574  logfacrlim  27578  logexprlim  27579  bposlem1  27638  bposlem2  27639  lgslem3  27653  lgsquadlem1  27734  lgsquadlem3  27736  chebbnd1lem3  27825  chtppilim  27829  chpchtlim  27833  dchrvmasumiflem1  27855  dchrisum0re  27867  mudivsum  27884  mulog2sumlem2  27889  pntibndlem2  27945  pntlemb  27951  pntlemh  27953  ostth3  27992  twocut  28836  addhalfcut  28872  recut  28907  crctcshwlkn0  30437  norm3lem  31778  nmopadjlem  32718  nmopcoadji  32730  hstle  32859  stadd3i  32877  strlem5  32884  pfxlsw2ccat  33580  elrgspnlem1  33870  vietadeg1  34277  locfinreflem  34539  xrge0iifcnv  34632  carsggect  35017  omsmeas  35022  signsply0  35247  signsvtp  35279  tgoldbachgtd  35358  1enumen  35804  sinccvglem  36603  faclim2  36690  poimirlem28  38757  ismblfin  38770  aks4d1p1p5  43316  sn-0lt1  43730  dffltz  43861  irrapxlem2  44021  pellexlem2  44028  areaquad  44408  dvgrat  45486  binomcxplemrat  45524  fmul01  46795  clim1fr1  46816  sinaover2ne0  47081  stoweidlem14  47227  stoweidlem16  47229  stoweidlem26  47239  stoweidlem41  47254  stoweidlem42  47255  stoweidlem45  47258  wallispi  47283  stirlinglem1  47287  stirlinglem12  47298  fourierdlem24  47344  fourierdlem107  47426  fouriersw  47444  meaiunincf  47696  meaiuninc3  47698  lincfsuppcl  49728  lincresunit3lem2  49795  lincresunit3  49796