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

Theorem 3eqtr3i 2466
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 2460 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2460 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1653
This theorem is referenced by:  csbvarg  3280  un12  3507  in12  3554  indif1  3587  difundi  3595  difundir  3596  difindi  3597  difindir  3598  dif32  3606  undif1  3705  orduniss2  4815  resmpt3  5194  xp0  5293  fresaunres2  5617  fvsnun1  5930  caov12  6277  caov13  6279  caov411  6281  caovdir  6283  fparlem3  6450  fparlem4  6451  hartogslem1  7513  kmlem3  8034  cdaassen  8064  xpcdaen  8065  halfnq  8855  reclem3pr  8928  addcmpblnr  8949  ltsrpr  8954  pn0sr  8978  sqgt0sr  8983  map2psrpr  8987  negsubdii  9387  halfpm6th  10194  i4  11485  nn0opthlem1  11563  fac4  11576  imi  11964  ef01bndlem  12787  bitsres  12987  gcdaddmlem  13030  modsubi  13410  gcdmodi  13412  numexpp1  13416  karatsuba  13422  oppgcntr  15163  frgpuplem  15406  ressmpladd  16522  ressmplmul  16523  ressmplvsca  16524  ltbwe  16535  ressply1add  16626  ressply1mul  16627  ressply1vsca  16628  sn0cld  17156  qtopres  17732  itg1addlem5  19594  cospi  20382  sincos4thpi  20423  sincos3rdpi  20426  dvlog  20544  dvlog2  20546  dvsqr  20630  ang180lem3  20655  1cubrlem  20683  mcubic  20689  quart1lem  20697  atantayl2  20780  log2cnv  20786  log2ublem2  20789  log2ub  20791  chtub  20998  bclbnd  21066  bposlem8  21077  lgsdir2lem1  21109  lgsdir2lem5  21113  ipidsq  22211  ip1ilem  22329  ipdirilem  22332  ipasslem10  22342  siilem1  22354  hvmul2negi  22552  hvadd12i  22561  hvnegdii  22566  normlem1  22614  normlem9  22622  normsubi  22645  normpar2i  22660  polid2i  22661  chjassi  22990  chj12i  23026  pjoml2i  23089  hoadd12i  23282  lnophmlem2  23522  nmopcoadj2i  23607  partfun  24089  sqsscirc1  24308  sigaclfu2  24506  coinflippvt  24744  ballotth  24797  gam1  24851  bpoly3  26106  onint1  26201  cnambfre  26257  rabren3dioph  26878  lhe4.4ex1a  27525  expgrowthi  27529  expgrowth  27531  dvcosre  27719  stoweidlem34  27761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator