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

Theorem 3eqtr3i 2324
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  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3i  |-  C  =  D

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3  |-  A  =  B
2 3eqtr3i.2 . . 3  |-  A  =  C
31, 2eqtr3i 2318 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2318 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  csbvarg  3121  un12  3346  in12  3393  indif1  3426  difundi  3434  difundir  3435  difindi  3436  difindir  3437  dif32  3444  undif1  3542  orduniss2  4640  resmpt3  5017  xp0  5114  fresaunres2  5429  fvsnun1  5731  caov12  6064  caov13  6066  caov411  6068  caovdir  6070  fparlem3  6236  fparlem4  6237  hartogslem1  7273  kmlem3  7794  cdaassen  7824  xpcdaen  7825  halfnq  8616  reclem3pr  8689  addcmpblnr  8710  ltsrpr  8715  pn0sr  8739  sqgt0sr  8744  map2psrpr  8748  negsubdii  9147  halfpm6th  9952  i4  11221  nn0opthlem1  11299  fac4  11312  imi  11658  ef01bndlem  12480  bitsres  12680  gcdaddmlem  12723  modsubi  13103  gcdmodi  13105  numexpp1  13109  karatsuba  13115  oppgcntr  14854  frgpuplem  15097  ressmpladd  16217  ressmplmul  16218  ressmplvsca  16219  ltbwe  16230  ressply1add  16324  ressply1mul  16325  ressply1vsca  16326  sn0cld  16843  qtopres  17405  itg1addlem5  19071  cospi  19856  sincos4thpi  19897  sincos3rdpi  19900  dvlog  20014  dvlog2  20016  dvsqr  20100  ang180lem3  20125  1cubrlem  20153  mcubic  20159  quart1lem  20167  atantayl2  20250  log2cnv  20256  log2ublem2  20259  log2ub  20261  chtub  20467  bclbnd  20535  bposlem8  20546  lgsdir2lem1  20578  lgsdir2lem5  20582  ipidsq  21302  ip1ilem  21420  ipdirilem  21423  ipasslem10  21433  siilem1  21445  hvmul2negi  21643  hvadd12i  21652  hvnegdii  21657  normlem1  21705  normlem9  21713  normsubi  21736  normpar2i  21751  polid2i  21752  chjassi  22081  chj12i  22117  pjoml2i  22180  hoadd12i  22373  lnophmlem2  22613  nmopcoadj2i  22698  sqsscirc1  23307  sigaclfu2  23497  coinflippvt  23700  bpoly3  24865  onint1  24960  rabren3dioph  27001  lhe4.4ex1a  27649  expgrowthi  27653  expgrowth  27655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator