Theorem breqtrdi 5207

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breqtrrdi  5208  difsnen  9119  marypha1lem  9502  en2eleq  10077  en2other2  10078  dju0en  10245  pwdju1  10260  pwdjudom  10284  ackbij1lem5  10292  alephadd  10646  prlem934  11102  ltexprlem2  11106  recgt0ii  12201  discr  14289  faclbnd4lem1  14342  hashfun  14486  01sqrexlem7  15297  resqrex  15299  abs3lemi  15459  supcvg  15904  ege2le3  16138  cos01gt0  16239  sin02gt0  16240  bitsfzolem  16480  bitsmod  16482  prmreclem2  16964  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  efgi0  19762  efgi1  19763  dprdf1  20077  metustexhalf  24590  nlmvscnlem2  24727  icccmplem2  24864  xrge0tsms  24875  iimulcl  24985  pcoass  25076  ipcnlem2  25297  ivthlem3  25507  vitalilem4  25665  vitali  25667  dvef  26038  ply1rem  26225  aaliou3lem2  26403  abelthlem8  26501  abelthlem9  26502  cosne0  26589  sinord  26594  tanregt0  26599  argimgt0  26672  logf1o2  26710  logtayllem  26719  cxpcn3lem  26808  ang180lem2  26871  ang180lem3  26872  atanlogsublem  26976  bndatandm  26990  leibpi  27003  emcllem6  27062  emcllem7  27063  lgamgulmlem5  27094  lgamcvg2  27116  ftalem5  27138  basellem7  27148  basellem9  27150  ppieq0  27237  ppiub  27266  chpeq0  27270  chpub  27282  logfacrlim  27286  logexprlim  27287  bposlem1  27346  bposlem2  27347  lgslem3  27361  lgsquadlem1  27442  lgsquadlem3  27444  chebbnd1lem3  27533  chtppilim  27537  chpchtlim  27541  dchrvmasumiflem1  27563  dchrisum0re  27575  mudivsum  27592  mulog2sumlem2  27597  pntibndlem2  27653  pntlemb  27659  pntlemh  27661  ostth3  27700  addhalfcut  28437  recut  28446  crctcshwlkn0  29854  norm3lem  31181  nmopadjlem  32121  nmopcoadji  32133  hstle  32262  stadd3i  32280  strlem5  32287  pfxlsw2ccat  32917  gsumle  33074  locfinreflem  33786  xrge0iifcnv  33879  carsggect  34283  omsmeas  34288  signsply0  34528  signsvtp  34560  tgoldbachgtd  34639  sinccvglem  35640  faclim2  35710  poimirlem28  37608  ismblfin  37621  aks4d1p1p5  42032  sn-0lt1  42439  sn-inelr  42443  dffltz  42589  irrapxlem2  42779  pellexlem2  42786  areaquad  43177  dvgrat  44281  binomcxplemrat  44319  fmul01  45501  clim1fr1  45522  sinaover2ne0  45789  stoweidlem14  45935  stoweidlem16  45937  stoweidlem26  45947  stoweidlem41  45962  stoweidlem42  45963  stoweidlem45  45966  wallispi  45991  stirlinglem1  45995  stirlinglem12  46006  fourierdlem24  46052  fourierdlem107  46134  fouriersw  46152  meaiunincf  46404  meaiuninc3  46406  lincfsuppcl  48142  lincresunit3lem2  48209  lincresunit3  48210