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

Syntax hints:   → wi 4   = wceq 1540   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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breqtrrdi  5190  difsnen  9056  marypha1lem  9431  en2eleq  10006  en2other2  10007  dju0en  10173  pwdju1  10188  pwdjudom  10214  ackbij1lem5  10222  alephadd  10575  prlem934  11031  ltexprlem2  11035  recgt0ii  12125  discr  14208  faclbnd4lem1  14258  hashfun  14402  01sqrexlem7  15200  resqrex  15202  abs3lemi  15362  supcvg  15807  ege2le3  16038  cos01gt0  16139  sin02gt0  16140  bitsfzolem  16380  bitsmod  16382  prmreclem2  16855  f1otrspeq  19357  pmtrf  19365  pmtrmvd  19366  pmtrfinv  19371  efgi0  19630  efgi1  19631  dprdf1  19945  metustexhalf  24286  nlmvscnlem2  24423  icccmplem2  24560  xrge0tsms  24571  iimulcl  24681  pcoass  24772  ipcnlem2  24993  ivthlem3  25203  vitalilem4  25361  vitali  25363  dvef  25733  ply1rem  25917  aaliou3lem2  26093  abelthlem8  26188  abelthlem9  26189  cosne0  26275  sinord  26280  tanregt0  26285  argimgt0  26357  logf1o2  26395  logtayllem  26404  cxpcn3lem  26492  ang180lem2  26552  ang180lem3  26553  atanlogsublem  26657  bndatandm  26671  leibpi  26684  emcllem6  26742  emcllem7  26743  lgamgulmlem5  26774  lgamcvg2  26796  ftalem5  26818  basellem7  26828  basellem9  26830  ppieq0  26917  ppiub  26944  chpeq0  26948  chpub  26960  logfacrlim  26964  logexprlim  26965  bposlem1  27024  bposlem2  27025  lgslem3  27039  lgsquadlem1  27120  lgsquadlem3  27122  chebbnd1lem3  27211  chtppilim  27215  chpchtlim  27219  dchrvmasumiflem1  27241  dchrisum0re  27253  mudivsum  27270  mulog2sumlem2  27275  pntibndlem2  27331  pntlemb  27337  pntlemh  27339  ostth3  27378  crctcshwlkn0  29343  norm3lem  30670  nmopadjlem  31610  nmopcoadji  31622  hstle  31751  stadd3i  31769  strlem5  31776  pfxlsw2ccat  32384  gsumle  32513  locfinreflem  33119  xrge0iifcnv  33212  carsggect  33616  omsmeas  33621  signsply0  33861  signsvtp  33893  tgoldbachgtd  33973  sinccvglem  34956  faclim2  35023  poimirlem28  36820  ismblfin  36833  aks4d1p1p5  41247  sn-0lt1  41638  sn-inelr  41641  dffltz  41679  irrapxlem2  41864  pellexlem2  41871  areaquad  42268  dvgrat  43374  binomcxplemrat  43412  fmul01  44595  clim1fr1  44616  sinaover2ne0  44883  stoweidlem14  45029  stoweidlem16  45031  stoweidlem26  45041  stoweidlem41  45056  stoweidlem42  45057  stoweidlem45  45060  wallispi  45085  stirlinglem1  45089  stirlinglem12  45100  fourierdlem24  45146  fourierdlem107  45228  fouriersw  45246  meaiunincf  45498  meaiuninc3  45500  lincfsuppcl  47182  lincresunit3lem2  47249  lincresunit3  47250