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

Syntax hints:   → wi 4   = wceq 1562   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 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breqtrrdi  5144  difsnen  9033  marypha1lem  9381  en2eleq  9966  en2other2  9967  dju0en  10134  pwdju1  10149  pwdjudom  10173  ackbij1lem5  10181  alephadd  10537  prlem934  10993  ltexprlem2  10997  recgt0ii  12100  discr  14255  faclbnd4lem1  14308  hashfun  14452  01sqrexlem7  15277  resqrex  15279  abs3lemi  15440  supcvg  15888  ege2le3  16122  cos01gt0  16225  sin02gt0  16226  bitsfzolem  16470  bitsmod  16472  prmreclem2  16955  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  efgi0  19762  efgi1  19763  dprdf1  20077  gsumle  20187  metustexhalf  24618  nlmvscnlem2  24747  icccmplem2  24886  xrge0tsms  24897  iimulcl  25001  pcoass  25088  ipcnlem2  25308  ivthlem3  25517  vitalilem4  25675  vitali  25677  dvef  26044  ply1rem  26228  aaliou3lem2  26409  abelthlem8  26504  abelthlem9  26505  cosne0  26596  sinord  26601  tanregt0  26606  argimgt0  26679  logf1o2  26717  logtayllem  26726  cxpcn3lem  26814  ang180lem2  26877  ang180lem3  26878  atanlogsublem  26982  bndatandm  26996  leibpi  27009  emcllem6  27067  emcllem7  27068  lgamgulmlem5  27099  lgamcvg2  27121  ftalem5  27143  basellem7  27153  basellem9  27155  ppieq0  27242  ppiub  27270  chpeq0  27274  chpub  27286  logfacrlim  27290  logexprlim  27291  bposlem1  27350  bposlem2  27351  lgslem3  27365  lgsquadlem1  27446  lgsquadlem3  27448  chebbnd1lem3  27537  chtppilim  27541  chpchtlim  27545  dchrvmasumiflem1  27567  dchrisum0re  27579  mudivsum  27596  mulog2sumlem2  27601  pntibndlem2  27657  pntlemb  27663  pntlemh  27665  ostth3  27704  twocut  28518  addhalfcut  28554  recut  28589  crctcshwlkn0  30023  norm3lem  31354  nmopadjlem  32294  nmopcoadji  32306  hstle  32435  stadd3i  32453  strlem5  32460  pfxlsw2ccat  33130  elrgspnlem1  33425  vietadeg1  33877  locfinreflem  34139  xrge0iifcnv  34232  carsggect  34617  omsmeas  34622  signsply0  34847  signsvtp  34879  tgoldbachgtd  34958  1enumen  35392  sinccvglem  36027  faclim2  36103  poimirlem28  38152  ismblfin  38165  aks4d1p1p5  42697  sn-0lt1  43102  dffltz  43221  irrapxlem2  43405  pellexlem2  43412  areaquad  43798  dvgrat  44893  binomcxplemrat  44931  fmul01  46161  clim1fr1  46182  sinaover2ne0  46447  stoweidlem14  46593  stoweidlem16  46595  stoweidlem26  46605  stoweidlem41  46620  stoweidlem42  46621  stoweidlem45  46624  wallispi  46649  stirlinglem1  46653  stirlinglem12  46664  fourierdlem24  46710  fourierdlem107  46792  fouriersw  46810  meaiunincf  47062  meaiuninc3  47064  lincfsuppcl  49040  lincresunit3lem2  49107  lincresunit3  49108