Theorem breqtrdi 5094

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

Syntax hints:   → wi 4   = wceq 1543   class class class wbr 5053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054

This theorem is referenced by:  breqtrrdi  5095  difsnen  8727  marypha1lem  9049  en2eleq  9622  en2other2  9623  dju0en  9789  pwdju1  9804  pwdjudom  9830  ackbij1lem5  9838  alephadd  10191  prlem934  10647  ltexprlem2  10651  recgt0ii  11738  discr  13807  faclbnd4lem1  13859  hashfun  14004  sqrlem7  14812  resqrex  14814  abs3lemi  14974  supcvg  15420  ege2le3  15651  cos01gt0  15752  sin02gt0  15753  bitsfzolem  15993  bitsmod  15995  prmreclem2  16470  f1otrspeq  18839  pmtrf  18847  pmtrmvd  18848  pmtrfinv  18853  efgi0  19110  efgi1  19111  dprdf1  19420  metustexhalf  23454  nlmvscnlem2  23583  icccmplem2  23720  xrge0tsms  23731  iimulcl  23834  pcoass  23921  ipcnlem2  24141  ivthlem3  24350  vitalilem4  24508  vitali  24510  dvef  24877  ply1rem  25061  aaliou3lem2  25236  abelthlem8  25331  abelthlem9  25332  cosne0  25418  sinord  25423  tanregt0  25428  argimgt0  25500  logf1o2  25538  logtayllem  25547  cxpcn3lem  25633  ang180lem2  25693  ang180lem3  25694  atanlogsublem  25798  bndatandm  25812  leibpi  25825  emcllem6  25883  emcllem7  25884  lgamgulmlem5  25915  lgamcvg2  25937  ftalem5  25959  basellem7  25969  basellem9  25971  ppieq0  26058  ppiub  26085  chpeq0  26089  chpub  26101  logfacrlim  26105  logexprlim  26106  bposlem1  26165  bposlem2  26166  lgslem3  26180  lgsquadlem1  26261  lgsquadlem3  26263  chebbnd1lem3  26352  chtppilim  26356  chpchtlim  26360  dchrvmasumiflem1  26382  dchrisum0re  26394  mudivsum  26411  mulog2sumlem2  26416  pntibndlem2  26472  pntlemb  26478  pntlemh  26480  ostth3  26519  crctcshwlkn0  27905  norm3lem  29230  nmopadjlem  30170  nmopcoadji  30182  hstle  30311  stadd3i  30329  strlem5  30336  pfxlsw2ccat  30944  gsumle  31069  locfinreflem  31504  xrge0iifcnv  31597  carsggect  31997  omsmeas  32002  signsply0  32242  signsvtp  32274  tgoldbachgtd  32354  sinccvglem  33343  faclim2  33432  poimirlem28  35542  ismblfin  35555  aks4d1p1p5  39816  sn-0lt1  40140  sn-inelr  40143  dffltz  40174  irrapxlem2  40348  pellexlem2  40355  areaquad  40750  dvgrat  41603  binomcxplemrat  41641  fmul01  42796  clim1fr1  42817  sinaover2ne0  43084  stoweidlem14  43230  stoweidlem16  43232  stoweidlem26  43242  stoweidlem41  43257  stoweidlem42  43258  stoweidlem45  43261  wallispi  43286  stirlinglem1  43290  stirlinglem12  43301  fourierdlem24  43347  fourierdlem107  43429  fouriersw  43447  meaiunincf  43696  meaiuninc3  43698  lincfsuppcl  45427  lincresunit3lem2  45494  lincresunit3  45495