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

Theorem breqtrdi 5147
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
StepHypRef Expression
1 breqtrdi.1 . 2 (𝜑𝐴𝑅𝐵)
2 eqid 2733 . 2 𝐴 = 𝐴
3 breqtrdi.2 . 2 𝐵 = 𝐶
41, 2, 33brtr3g 5139 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  breqtrrdi  5148  difsnen  9000  marypha1lem  9374  en2eleq  9949  en2other2  9950  dju0en  10116  pwdju1  10131  pwdjudom  10157  ackbij1lem5  10165  alephadd  10518  prlem934  10974  ltexprlem2  10978  recgt0ii  12066  discr  14149  faclbnd4lem1  14199  hashfun  14343  01sqrexlem7  15139  resqrex  15141  abs3lemi  15301  supcvg  15746  ege2le3  15977  cos01gt0  16078  sin02gt0  16079  bitsfzolem  16319  bitsmod  16321  prmreclem2  16794  f1otrspeq  19234  pmtrf  19242  pmtrmvd  19243  pmtrfinv  19248  efgi0  19507  efgi1  19508  dprdf1  19817  metustexhalf  23928  nlmvscnlem2  24065  icccmplem2  24202  xrge0tsms  24213  iimulcl  24316  pcoass  24403  ipcnlem2  24624  ivthlem3  24833  vitalilem4  24991  vitali  24993  dvef  25360  ply1rem  25544  aaliou3lem2  25719  abelthlem8  25814  abelthlem9  25815  cosne0  25901  sinord  25906  tanregt0  25911  argimgt0  25983  logf1o2  26021  logtayllem  26030  cxpcn3lem  26116  ang180lem2  26176  ang180lem3  26177  atanlogsublem  26281  bndatandm  26295  leibpi  26308  emcllem6  26366  emcllem7  26367  lgamgulmlem5  26398  lgamcvg2  26420  ftalem5  26442  basellem7  26452  basellem9  26454  ppieq0  26541  ppiub  26568  chpeq0  26572  chpub  26584  logfacrlim  26588  logexprlim  26589  bposlem1  26648  bposlem2  26649  lgslem3  26663  lgsquadlem1  26744  lgsquadlem3  26746  chebbnd1lem3  26835  chtppilim  26839  chpchtlim  26843  dchrvmasumiflem1  26865  dchrisum0re  26877  mudivsum  26894  mulog2sumlem2  26899  pntibndlem2  26955  pntlemb  26961  pntlemh  26963  ostth3  27002  crctcshwlkn0  28808  norm3lem  30133  nmopadjlem  31073  nmopcoadji  31085  hstle  31214  stadd3i  31232  strlem5  31239  pfxlsw2ccat  31855  gsumle  31981  locfinreflem  32478  xrge0iifcnv  32571  carsggect  32975  omsmeas  32980  signsply0  33220  signsvtp  33252  tgoldbachgtd  33332  sinccvglem  34317  faclim2  34377  poimirlem28  36152  ismblfin  36165  aks4d1p1p5  40578  sn-0lt1  40974  sn-inelr  40977  dffltz  41015  irrapxlem2  41189  pellexlem2  41196  areaquad  41593  dvgrat  42680  binomcxplemrat  42718  fmul01  43907  clim1fr1  43928  sinaover2ne0  44195  stoweidlem14  44341  stoweidlem16  44343  stoweidlem26  44353  stoweidlem41  44368  stoweidlem42  44369  stoweidlem45  44372  wallispi  44397  stirlinglem1  44401  stirlinglem12  44412  fourierdlem24  44458  fourierdlem107  44540  fouriersw  44558  meaiunincf  44810  meaiuninc3  44812  lincfsuppcl  46580  lincresunit3lem2  46647  lincresunit3  46648
  Copyright terms: Public domain W3C validator