Theorem syl6breq 4694

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

Hypotheses

Ref	Expression
syl6breq.1	|- ( ph -> A R B )
syl6breq.2	|- B = C

Assertion

Ref	Expression
syl6breq	|- ( ph -> A R C )

Proof of Theorem syl6breq

Step	Hyp	Ref	Expression
1		syl6breq.1	. 2 |- ( ph -> A R B )
2		eqid 2622	. 2 |- A = A
3		syl6breq.2	. 2 |- B = C
4	1, 2, 3	3brtr3g 4686	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  syl6breqr  4695  difsnen  8042  marypha1lem  8339  en2eleq  8831  en2other2  8832  cda0en  9001  ackbij1lem5  9046  alephadd  9399  prlem934  9855  ltexprlem2  9859  recgt0ii  10929  discr  13001  faclbnd4lem1  13080  hashfun  13224  sqrlem7  13989  resqrex  13991  abs3lemi  14149  supcvg  14588  ege2le3  14820  cos01gt0  14921  sin02gt0  14922  bitsfzolem  15156  bitsmod  15158  prmreclem2  15621  f1otrspeq  17867  pmtrf  17875  pmtrmvd  17876  pmtrfinv  17881  efgi0  18133  efgi1  18134  dprdf1  18432  metustexhalf  22361  nlmvscnlem2  22489  icccmplem2  22626  xrge0tsms  22637  iimulcl  22736  pcoass  22824  ipcnlem2  23043  ivthlem3  23222  vitalilem4  23380  vitali  23382  dvef  23743  ply1rem  23923  aaliou3lem2  24098  abelthlem8  24193  abelthlem9  24194  cosne0  24276  sinord  24280  tanregt0  24285  argimgt0  24358  logf1o2  24396  logtayllem  24405  cxpcn3lem  24488  ang180lem2  24540  ang180lem3  24541  atanlogsublem  24642  bndatandm  24656  leibpi  24669  emcllem6  24727  emcllem7  24728  lgamgulmlem5  24759  lgamcvg2  24781  ftalem5  24803  basellem7  24813  basellem9  24815  ppieq0  24902  ppiub  24929  chpeq0  24933  chpub  24945  logfacrlim  24949  logexprlim  24950  bposlem1  25009  bposlem2  25010  lgslem3  25024  lgsquadlem1  25105  lgsquadlem3  25107  chebbnd1lem3  25160  chtppilim  25164  chpchtlim  25168  dchrvmasumiflem1  25190  dchrisum0re  25202  mudivsum  25219  mulog2sumlem2  25224  pntibndlem2  25280  pntlemb  25286  pntlemh  25288  ostth3  25327  crctcshwlkn0  26713  norm3lem  28006  nmopadjlem  28948  nmopcoadji  28960  hstle  29089  stadd3i  29107  strlem5  29114  gsumle  29779  locfinreflem  29907  xrge0iifcnv  29979  carsggect  30380  omsmeas  30385  signsply0  30628  signsvtp  30660  tgoldbachgtd  30740  sinccvglem  31566  faclim2  31634  poimirlem28  33437  ismblfin  33450  irrapxlem2  37387  pellexlem2  37394  areaquad  37802  dvgrat  38511  binomcxplemrat  38549  fmul01  39812  clim1fr1  39833  sinaover2ne0  40079  stoweidlem14  40231  stoweidlem16  40233  stoweidlem26  40243  stoweidlem41  40258  stoweidlem42  40259  stoweidlem45  40262  wallispi  40287  stirlinglem1  40291  stirlinglem12  40302  fourierdlem24  40348  fourierdlem107  40430  fouriersw  40448  lincfsuppcl  42202  lincresunit3lem2  42269  lincresunit3  42270