Theorem breqtrdi 5189

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  breqtrrdi  5190  difsnen  9092  marypha1lem  9471  en2eleq  10046  en2other2  10047  dju0en  10214  pwdju1  10229  pwdjudom  10253  ackbij1lem5  10261  alephadd  10615  prlem934  11071  ltexprlem2  11075  recgt0ii  12172  discr  14276  faclbnd4lem1  14329  hashfun  14473  01sqrexlem7  15284  resqrex  15286  abs3lemi  15446  supcvg  15889  ege2le3  16123  cos01gt0  16224  sin02gt0  16225  bitsfzolem  16468  bitsmod  16470  prmreclem2  16951  f1otrspeq  19480  pmtrf  19488  pmtrmvd  19489  pmtrfinv  19494  efgi0  19753  efgi1  19754  dprdf1  20068  metustexhalf  24585  nlmvscnlem2  24722  icccmplem2  24859  xrge0tsms  24870  iimulcl  24980  pcoass  25071  ipcnlem2  25292  ivthlem3  25502  vitalilem4  25660  vitali  25662  dvef  26033  ply1rem  26220  aaliou3lem2  26400  abelthlem8  26498  abelthlem9  26499  cosne0  26586  sinord  26591  tanregt0  26596  argimgt0  26669  logf1o2  26707  logtayllem  26716  cxpcn3lem  26805  ang180lem2  26868  ang180lem3  26869  atanlogsublem  26973  bndatandm  26987  leibpi  27000  emcllem6  27059  emcllem7  27060  lgamgulmlem5  27091  lgamcvg2  27113  ftalem5  27135  basellem7  27145  basellem9  27147  ppieq0  27234  ppiub  27263  chpeq0  27267  chpub  27279  logfacrlim  27283  logexprlim  27284  bposlem1  27343  bposlem2  27344  lgslem3  27358  lgsquadlem1  27439  lgsquadlem3  27441  chebbnd1lem3  27530  chtppilim  27534  chpchtlim  27538  dchrvmasumiflem1  27560  dchrisum0re  27572  mudivsum  27589  mulog2sumlem2  27594  pntibndlem2  27650  pntlemb  27656  pntlemh  27658  ostth3  27697  addhalfcut  28434  recut  28443  crctcshwlkn0  29851  norm3lem  31178  nmopadjlem  32118  nmopcoadji  32130  hstle  32259  stadd3i  32277  strlem5  32284  pfxlsw2ccat  32920  gsumle  33084  elrgspnlem1  33232  locfinreflem  33801  xrge0iifcnv  33894  carsggect  34300  omsmeas  34305  signsply0  34545  signsvtp  34577  tgoldbachgtd  34656  sinccvglem  35657  faclim2  35728  poimirlem28  37635  ismblfin  37648  aks4d1p1p5  42057  sn-0lt1  42470  sn-inelr  42474  dffltz  42621  irrapxlem2  42811  pellexlem2  42818  areaquad  43205  dvgrat  44308  binomcxplemrat  44346  fmul01  45536  clim1fr1  45557  sinaover2ne0  45824  stoweidlem14  45970  stoweidlem16  45972  stoweidlem26  45982  stoweidlem41  45997  stoweidlem42  45998  stoweidlem45  46001  wallispi  46026  stirlinglem1  46030  stirlinglem12  46041  fourierdlem24  46087  fourierdlem107  46169  fouriersw  46187  meaiunincf  46439  meaiuninc3  46441  lincfsuppcl  48259  lincresunit3lem2  48326  lincresunit3  48327