Theorem breqtrdi 5143

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtrrdi  5144  difsnen  9000  marypha1lem  9360  en2eleq  9939  en2other2  9940  dju0en  10107  pwdju1  10122  pwdjudom  10146  ackbij1lem5  10154  alephadd  10508  prlem934  10964  ltexprlem2  10968  recgt0ii  12067  discr  14183  faclbnd4lem1  14236  hashfun  14380  01sqrexlem7  15191  resqrex  15193  abs3lemi  15354  supcvg  15799  ege2le3  16033  cos01gt0  16136  sin02gt0  16137  bitsfzolem  16381  bitsmod  16383  prmreclem2  16865  f1otrspeq  19362  pmtrf  19370  pmtrmvd  19371  pmtrfinv  19376  efgi0  19635  efgi1  19636  dprdf1  19950  gsumle  20060  metustexhalf  24478  nlmvscnlem2  24607  icccmplem2  24746  xrge0tsms  24757  iimulcl  24867  pcoass  24958  ipcnlem2  25178  ivthlem3  25388  vitalilem4  25546  vitali  25548  dvef  25918  ply1rem  26105  aaliou3lem2  26285  abelthlem8  26383  abelthlem9  26384  cosne0  26472  sinord  26477  tanregt0  26482  argimgt0  26555  logf1o2  26593  logtayllem  26602  cxpcn3lem  26691  ang180lem2  26754  ang180lem3  26755  atanlogsublem  26859  bndatandm  26873  leibpi  26886  emcllem6  26945  emcllem7  26946  lgamgulmlem5  26977  lgamcvg2  26999  ftalem5  27021  basellem7  27031  basellem9  27033  ppieq0  27120  ppiub  27149  chpeq0  27153  chpub  27165  logfacrlim  27169  logexprlim  27170  bposlem1  27229  bposlem2  27230  lgslem3  27244  lgsquadlem1  27325  lgsquadlem3  27327  chebbnd1lem3  27416  chtppilim  27420  chpchtlim  27424  dchrvmasumiflem1  27446  dchrisum0re  27458  mudivsum  27475  mulog2sumlem2  27480  pntibndlem2  27536  pntlemb  27542  pntlemh  27544  ostth3  27583  twocut  28351  addhalfcut  28383  recut  28401  crctcshwlkn0  29802  norm3lem  31129  nmopadjlem  32069  nmopcoadji  32081  hstle  32210  stadd3i  32228  strlem5  32235  pfxlsw2ccat  32923  elrgspnlem1  33210  locfinreflem  33824  xrge0iifcnv  33917  carsggect  34303  omsmeas  34308  signsply0  34536  signsvtp  34568  tgoldbachgtd  34647  sinccvglem  35653  faclim2  35729  poimirlem28  37636  ismblfin  37649  aks4d1p1p5  42057  sn-0lt1  42457  dffltz  42616  irrapxlem2  42805  pellexlem2  42812  areaquad  43199  dvgrat  44295  binomcxplemrat  44333  fmul01  45572  clim1fr1  45593  sinaover2ne0  45860  stoweidlem14  46006  stoweidlem16  46008  stoweidlem26  46018  stoweidlem41  46033  stoweidlem42  46034  stoweidlem45  46037  wallispi  46062  stirlinglem1  46066  stirlinglem12  46077  fourierdlem24  46123  fourierdlem107  46205  fouriersw  46223  meaiunincf  46475  meaiuninc3  46477  lincfsuppcl  48396  lincresunit3lem2  48463  lincresunit3  48464