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

Theorem 3eqtr3i 2782
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3i.1 𝐴 = 𝐵
3eqtr3i.2 𝐴 = 𝐶
3eqtr3i.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3i 𝐶 = 𝐷

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3 𝐴 = 𝐵
2 3eqtr3i.2 . . 3 𝐴 = 𝐶
31, 2eqtr3i 2776 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2776 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745
This theorem is referenced by:  un12  3906  in12  3959  indif1  4006  difundi  4014  difundir  4015  difindi  4016  difindir  4017  dif32  4026  csbvarg  4138  undif1  4179  resmpt3  5600  xp0  5702  fresaunres2  6229  fvsnun1  6604  caov12  7019  caov13  7021  caov411  7023  caovdir  7025  orduniss2  7190  fparlem3  7439  fparlem4  7440  hartogslem1  8604  kmlem3  9158  cdaassen  9188  xpcdaen  9189  halfnq  9982  reclem3pr  10055  addcmpblnr  10074  ltsrpr  10082  pn0sr  10106  sqgt0sr  10111  map2psrpr  10115  negsubdii  10550  halfpm6th  11437  decmul1  11769  i4  13153  nn0opthlem1  13241  fac4  13254  imi  14088  bpoly3  14980  ef01bndlem  15105  bitsres  15389  gcdaddmlem  15439  modsubi  15970  gcdmodi  15972  numexpp1  15976  karatsuba  15986  karatsubaOLD  15987  oppgcntr  17987  frgpuplem  18377  ressmpladd  19651  ressmplmul  19652  ressmplvsca  19653  ltbwe  19666  ressply1add  19794  ressply1mul  19795  ressply1vsca  19796  sn0cld  21088  qtopres  21695  itg1addlem5  23658  cospi  24415  sincos4thpi  24456  sincos3rdpi  24459  dvlog  24588  dvlog2  24590  dvsqrt  24674  dvcnsqrt  24676  ang180lem3  24732  1cubrlem  24759  mcubic  24765  quart1lem  24773  atantayl2  24856  log2cnv  24862  log2ublem2  24865  log2ub  24867  gam1  24982  chtub  25128  bclbnd  25196  bposlem8  25207  lgsdir2lem1  25241  lgsdir2lem5  25245  2lgsoddprmlem3d  25329  ex-bc  27612  ex-gcd  27617  ipidsq  27866  ip1ilem  27982  ipdirilem  27985  ipasslem10  27995  siilem1  28007  hvmul2negi  28206  hvadd12i  28215  hvnegdii  28220  normlem1  28268  normlem9  28276  normsubi  28299  normpar2i  28314  polid2i  28315  chjassi  28646  chj12i  28682  pjoml2i  28745  hoadd12i  28937  lnophmlem2  29177  nmopcoadj2i  29262  indifundif  29655  aciunf1  29764  partfun  29776  ffsrn  29805  dpmul10  29904  dpmul1000  29908  dpadd2  29919  dpadd  29920  dpmul  29922  archirngz  30044  sqsscirc1  30255  sigaclfu2  30485  eulerpartlemd  30729  coinflippvt  30847  ballotth  30900  hgt750lem  31030  hgt750lem2  31031  quad3  31863  onint1  32746  bj-csbsn  33197  cnambfre  33763  rabren3dioph  37873  arearect  38295  areaquad  38296  resnonrel  38392  cononrel1  38394  cononrel2  38395  lhe4.4ex1a  39022  expgrowthi  39026  expgrowth  39028  binomcxplemnotnn0  39049  liminf0  40520  dvcosre  40621  stoweidlem34  40746  fouriersw  40943
  Copyright terms: Public domain W3C validator