Theorem breqtrdi 5188

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5147

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  breqtrrdi  5189  difsnen  9055  marypha1lem  9430  en2eleq  10005  en2other2  10006  dju0en  10172  pwdju1  10187  pwdjudom  10213  ackbij1lem5  10221  alephadd  10574  prlem934  11030  ltexprlem2  11034  recgt0ii  12124  discr  14207  faclbnd4lem1  14257  hashfun  14401  01sqrexlem7  15199  resqrex  15201  abs3lemi  15361  supcvg  15806  ege2le3  16037  cos01gt0  16138  sin02gt0  16139  bitsfzolem  16379  bitsmod  16381  prmreclem2  16854  f1otrspeq  19356  pmtrf  19364  pmtrmvd  19365  pmtrfinv  19370  efgi0  19629  efgi1  19630  dprdf1  19944  metustexhalf  24285  nlmvscnlem2  24422  icccmplem2  24559  xrge0tsms  24570  iimulcl  24680  pcoass  24771  ipcnlem2  24992  ivthlem3  25202  vitalilem4  25360  vitali  25362  dvef  25732  ply1rem  25916  aaliou3lem2  26092  abelthlem8  26187  abelthlem9  26188  cosne0  26274  sinord  26279  tanregt0  26284  argimgt0  26356  logf1o2  26394  logtayllem  26403  cxpcn3lem  26491  ang180lem2  26551  ang180lem3  26552  atanlogsublem  26656  bndatandm  26670  leibpi  26683  emcllem6  26741  emcllem7  26742  lgamgulmlem5  26773  lgamcvg2  26795  ftalem5  26817  basellem7  26827  basellem9  26829  ppieq0  26916  ppiub  26943  chpeq0  26947  chpub  26959  logfacrlim  26963  logexprlim  26964  bposlem1  27023  bposlem2  27024  lgslem3  27038  lgsquadlem1  27119  lgsquadlem3  27121  chebbnd1lem3  27210  chtppilim  27214  chpchtlim  27218  dchrvmasumiflem1  27240  dchrisum0re  27252  mudivsum  27269  mulog2sumlem2  27274  pntibndlem2  27330  pntlemb  27336  pntlemh  27338  ostth3  27377  crctcshwlkn0  29342  norm3lem  30669  nmopadjlem  31609  nmopcoadji  31621  hstle  31750  stadd3i  31768  strlem5  31775  pfxlsw2ccat  32383  gsumle  32512  locfinreflem  33118  xrge0iifcnv  33211  carsggect  33615  omsmeas  33620  signsply0  33860  signsvtp  33892  tgoldbachgtd  33972  sinccvglem  34955  faclim2  35022  poimirlem28  36819  ismblfin  36832  aks4d1p1p5  41246  sn-0lt1  41637  sn-inelr  41640  dffltz  41678  irrapxlem2  41863  pellexlem2  41870  areaquad  42267  dvgrat  43373  binomcxplemrat  43411  fmul01  44594  clim1fr1  44615  sinaover2ne0  44882  stoweidlem14  45028  stoweidlem16  45030  stoweidlem26  45040  stoweidlem41  45055  stoweidlem42  45056  stoweidlem45  45059  wallispi  45084  stirlinglem1  45088  stirlinglem12  45099  fourierdlem24  45145  fourierdlem107  45227  fouriersw  45245  meaiunincf  45497  meaiuninc3  45499  lincfsuppcl  47181  lincresunit3lem2  47248  lincresunit3  47249