MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6breq Structured version   Visualization version   GIF version

Theorem syl6breq 4624
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
StepHypRef Expression
1 syl6breq.1 . 2 (𝜑𝐴𝑅𝐵)
2 eqid 2610 . 2 𝐴 = 𝐴
3 syl6breq.2 . 2 𝐵 = 𝐶
41, 2, 33brtr3g 4616 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  syl6breqr  4625  difsnen  7927  marypha1lem  8222  en2eleq  8714  en2other2  8715  cda0en  8884  ackbij1lem5  8929  alephadd  9278  prlem934  9734  ltexprlem2  9738  recgt0ii  10808  discr  12863  faclbnd4lem1  12942  hashfun  13084  sqrlem7  13837  resqrex  13839  abs3lemi  13997  supcvg  14427  ege2le3  14659  cos01gt0  14760  sin02gt0  14761  bitsfzolem  14994  bitsmod  14996  prmreclem2  15459  f1otrspeq  17690  pmtrf  17698  pmtrmvd  17699  pmtrfinv  17704  efgi0  17956  efgi1  17957  dprdf1  18255  metustexhalf  22171  nlmvscnlem2  22299  icccmplem2  22434  xrge0tsms  22445  iimulcl  22544  pcoass  22632  ipcnlem2  22851  ivthlem3  23029  vitalilem4  23186  vitali  23188  dvef  23547  ply1rem  23727  aaliou3lem2  23902  abelthlem8  23997  abelthlem9  23998  cosne0  24080  sinord  24084  tanregt0  24089  argimgt0  24162  logf1o2  24196  logtayllem  24205  cxpcn3lem  24288  ang180lem2  24340  ang180lem3  24341  atanlogsublem  24442  bndatandm  24456  leibpi  24469  emcllem6  24527  emcllem7  24528  lgamgulmlem5  24559  lgamcvg2  24581  ftalem5  24603  basellem7  24613  basellem9  24615  ppieq0  24702  ppiub  24729  chpeq0  24733  chpub  24745  logfacrlim  24749  logexprlim  24750  bposlem1  24809  bposlem2  24810  lgslem3  24824  lgsquadlem1  24905  lgsquadlem3  24907  chebbnd1lem3  24960  chtppilim  24964  chpchtlim  24968  dchrvmasumiflem1  24990  dchrisum0re  25002  mudivsum  25019  mulog2sumlem2  25024  pntibndlem2  25080  pntlemb  25086  pntlemh  25088  ostth3  25127  norm3lem  27390  nmopadjlem  28332  nmopcoadji  28344  hstle  28473  stadd3i  28491  strlem5  28498  gsumle  29110  locfinreflem  29235  xrge0iifcnv  29307  carsggect  29707  omsmeas  29712  signsply0  29954  signsvtp  29986  sinccvglem  30820  faclim2  30887  poimirlem28  32607  ismblfin  32620  irrapxlem2  36405  pellexlem2  36412  areaquad  36821  dvgrat  37533  binomcxplemrat  37571  fmul01  38647  clim1fr1  38668  sinaover2ne0  38751  stoweidlem14  38907  stoweidlem16  38909  stoweidlem26  38919  stoweidlem41  38934  stoweidlem42  38935  stoweidlem45  38938  wallispi  38963  stirlinglem1  38967  stirlinglem12  38978  fourierdlem24  39024  fourierdlem107  39106  fouriersw  39124  crctcsh1wlkn0  41024  lincfsuppcl  41996  lincresunit3lem2  42063  lincresunit3  42064
  Copyright terms: Public domain W3C validator