Theorem breqtrdi 5184

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144

This theorem is referenced by:  breqtrrdi  5185  difsnen  9072  marypha1lem  9451  en2eleq  10026  en2other2  10027  dju0en  10193  pwdju1  10208  pwdjudom  10234  ackbij1lem5  10242  alephadd  10595  prlem934  11051  ltexprlem2  11055  recgt0ii  12145  discr  14229  faclbnd4lem1  14279  hashfun  14423  01sqrexlem7  15222  resqrex  15224  abs3lemi  15384  supcvg  15829  ege2le3  16061  cos01gt0  16162  sin02gt0  16163  bitsfzolem  16403  bitsmod  16405  prmreclem2  16880  f1otrspeq  19396  pmtrf  19404  pmtrmvd  19405  pmtrfinv  19410  efgi0  19669  efgi1  19670  dprdf1  19984  metustexhalf  24459  nlmvscnlem2  24596  icccmplem2  24733  xrge0tsms  24744  iimulcl  24854  pcoass  24945  ipcnlem2  25166  ivthlem3  25376  vitalilem4  25534  vitali  25536  dvef  25906  ply1rem  26094  aaliou3lem2  26272  abelthlem8  26370  abelthlem9  26371  cosne0  26457  sinord  26462  tanregt0  26467  argimgt0  26540  logf1o2  26578  logtayllem  26587  cxpcn3lem  26676  ang180lem2  26736  ang180lem3  26737  atanlogsublem  26841  bndatandm  26855  leibpi  26868  emcllem6  26927  emcllem7  26928  lgamgulmlem5  26959  lgamcvg2  26981  ftalem5  27003  basellem7  27013  basellem9  27015  ppieq0  27102  ppiub  27131  chpeq0  27135  chpub  27147  logfacrlim  27151  logexprlim  27152  bposlem1  27211  bposlem2  27212  lgslem3  27226  lgsquadlem1  27307  lgsquadlem3  27309  chebbnd1lem3  27398  chtppilim  27402  chpchtlim  27406  dchrvmasumiflem1  27428  dchrisum0re  27440  mudivsum  27457  mulog2sumlem2  27462  pntibndlem2  27518  pntlemb  27524  pntlemh  27526  ostth3  27565  recut  28218  crctcshwlkn0  29626  norm3lem  30953  nmopadjlem  31893  nmopcoadji  31905  hstle  32034  stadd3i  32052  strlem5  32059  pfxlsw2ccat  32668  gsumle  32799  locfinreflem  33436  xrge0iifcnv  33529  carsggect  33933  omsmeas  33938  signsply0  34178  signsvtp  34210  tgoldbachgtd  34289  sinccvglem  35271  faclim2  35337  poimirlem28  37116  ismblfin  37129  aks4d1p1p5  41541  sn-0lt1  42008  sn-inelr  42011  dffltz  42049  irrapxlem2  42234  pellexlem2  42241  areaquad  42635  dvgrat  43740  binomcxplemrat  43778  fmul01  44959  clim1fr1  44980  sinaover2ne0  45247  stoweidlem14  45393  stoweidlem16  45395  stoweidlem26  45405  stoweidlem41  45420  stoweidlem42  45421  stoweidlem45  45424  wallispi  45449  stirlinglem1  45453  stirlinglem12  45464  fourierdlem24  45510  fourierdlem107  45592  fouriersw  45610  meaiunincf  45862  meaiuninc3  45864  lincfsuppcl  47472  lincresunit3lem2  47539  lincresunit3  47540