Theorem syl6breq 4927

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
syl6breq.1	⊢ (𝜑 → 𝐴𝑅𝐵)
syl6breq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6breq	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl6breq

Step	Hyp	Ref	Expression
1		syl6breq.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		eqid 2777	. 2 ⊢ 𝐴 = 𝐴
3		syl6breq.2	. 2 ⊢ 𝐵 = 𝐶
4	1, 2, 3	3brtr3g 4919	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1601   class class class wbr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4887

This theorem is referenced by:  syl6breqr  4928  difsnen  8330  marypha1lem  8627  en2eleq  9164  en2other2  9165  cda0en  9336  alephadd  9734  prlem934  10190  ltexprlem2  10194  recgt0ii  11283  discr  13320  faclbnd4lem1  13398  hashfun  13538  sqrlem7  14396  resqrex  14398  abs3lemi  14557  supcvg  14992  ege2le3  15222  cos01gt0  15323  sin02gt0  15324  bitsfzolem  15562  bitsmod  15564  prmreclem2  16025  f1otrspeq  18250  pmtrf  18258  pmtrmvd  18259  pmtrfinv  18264  efgi0  18517  efgi1  18518  dprdf1  18819  metustexhalf  22769  nlmvscnlem2  22897  icccmplem2  23034  xrge0tsms  23045  iimulcl  23144  pcoass  23231  ipcnlem2  23450  ivthlem3  23657  vitalilem4  23815  vitali  23817  dvef  24180  ply1rem  24360  aaliou3lem2  24535  abelthlem8  24630  abelthlem9  24631  cosne0  24714  sinord  24718  tanregt0  24723  argimgt0  24795  logf1o2  24833  logtayllem  24842  cxpcn3lem  24928  ang180lem2  24988  ang180lem3  24989  atanlogsublem  25093  bndatandm  25107  leibpi  25121  emcllem6  25179  emcllem7  25180  lgamgulmlem5  25211  lgamcvg2  25233  ftalem5  25255  basellem7  25265  basellem9  25267  ppieq0  25354  ppiub  25381  chpeq0  25385  chpub  25397  logfacrlim  25401  logexprlim  25402  bposlem1  25461  bposlem2  25462  lgslem3  25476  lgsquadlem1  25557  lgsquadlem3  25559  chebbnd1lem3  25612  chtppilim  25616  chpchtlim  25620  dchrvmasumiflem1  25642  dchrisum0re  25654  mudivsum  25671  mulog2sumlem2  25676  pntibndlem2  25732  pntlemb  25738  pntlemh  25740  ostth3  25779  crctcshwlkn0  27170  norm3lem  28578  nmopadjlem  29520  nmopcoadji  29532  hstle  29661  stadd3i  29679  strlem5  29686  gsumle  30341  locfinreflem  30505  xrge0iifcnv  30577  carsggect  30978  omsmeas  30983  signsply0  31228  signsvtp  31262  tgoldbachgtd  31342  sinccvglem  32163  faclim2  32228  poimirlem28  34058  ismblfin  34071  dffltz  38206  irrapxlem2  38340  pellexlem2  38347  areaquad  38753  dvgrat  39460  binomcxplemrat  39498  fmul01  40713  clim1fr1  40734  sinaover2ne0  41000  stoweidlem14  41151  stoweidlem16  41153  stoweidlem26  41163  stoweidlem41  41178  stoweidlem42  41179  stoweidlem45  41182  wallispi  41207  stirlinglem1  41211  stirlinglem12  41222  fourierdlem24  41268  fourierdlem107  41350  fouriersw  41368  meaiunincf  41617  meaiuninc3  41619  lincfsuppcl  43210  lincresunit3lem2  43277  lincresunit3  43278