Theorem breqtrdi 5165

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  breqtrrdi  5166  difsnen  9072  marypha1lem  9450  en2eleq  10027  en2other2  10028  dju0en  10195  pwdju1  10210  pwdjudom  10234  ackbij1lem5  10242  alephadd  10596  prlem934  11052  ltexprlem2  11056  recgt0ii  12153  discr  14263  faclbnd4lem1  14316  hashfun  14460  01sqrexlem7  15272  resqrex  15274  abs3lemi  15434  supcvg  15877  ege2le3  16111  cos01gt0  16214  sin02gt0  16215  bitsfzolem  16458  bitsmod  16460  prmreclem2  16942  f1otrspeq  19433  pmtrf  19441  pmtrmvd  19442  pmtrfinv  19447  efgi0  19706  efgi1  19707  dprdf1  20021  metustexhalf  24500  nlmvscnlem2  24629  icccmplem2  24768  xrge0tsms  24779  iimulcl  24889  pcoass  24980  ipcnlem2  25201  ivthlem3  25411  vitalilem4  25569  vitali  25571  dvef  25941  ply1rem  26128  aaliou3lem2  26308  abelthlem8  26406  abelthlem9  26407  cosne0  26495  sinord  26500  tanregt0  26505  argimgt0  26578  logf1o2  26616  logtayllem  26625  cxpcn3lem  26714  ang180lem2  26777  ang180lem3  26778  atanlogsublem  26882  bndatandm  26896  leibpi  26909  emcllem6  26968  emcllem7  26969  lgamgulmlem5  27000  lgamcvg2  27022  ftalem5  27044  basellem7  27054  basellem9  27056  ppieq0  27143  ppiub  27172  chpeq0  27176  chpub  27188  logfacrlim  27192  logexprlim  27193  bposlem1  27252  bposlem2  27253  lgslem3  27267  lgsquadlem1  27348  lgsquadlem3  27350  chebbnd1lem3  27439  chtppilim  27443  chpchtlim  27447  dchrvmasumiflem1  27469  dchrisum0re  27481  mudivsum  27498  mulog2sumlem2  27503  pntibndlem2  27559  pntlemb  27565  pntlemh  27567  ostth3  27606  twocut  28366  addhalfcut  28391  recut  28404  crctcshwlkn0  29808  norm3lem  31135  nmopadjlem  32075  nmopcoadji  32087  hstle  32216  stadd3i  32234  strlem5  32241  pfxlsw2ccat  32931  gsumle  33097  elrgspnlem1  33242  locfinreflem  33876  xrge0iifcnv  33969  carsggect  34355  omsmeas  34360  signsply0  34588  signsvtp  34620  tgoldbachgtd  34699  sinccvglem  35699  faclim2  35770  poimirlem28  37677  ismblfin  37690  aks4d1p1p5  42093  sn-0lt1  42481  sn-inelr  42485  dffltz  42632  irrapxlem2  42821  pellexlem2  42828  areaquad  43215  dvgrat  44311  binomcxplemrat  44349  fmul01  45589  clim1fr1  45610  sinaover2ne0  45877  stoweidlem14  46023  stoweidlem16  46025  stoweidlem26  46035  stoweidlem41  46050  stoweidlem42  46051  stoweidlem45  46054  wallispi  46079  stirlinglem1  46083  stirlinglem12  46094  fourierdlem24  46140  fourierdlem107  46222  fouriersw  46240  meaiunincf  46492  meaiuninc3  46494  lincfsuppcl  48369  lincresunit3lem2  48436  lincresunit3  48437