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

Theorem 3eqtr3i 2469
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 2463 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2463 1  |-  C  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  un12  3511  in12  3558  indif1  3591  difundi  3599  difundir  3600  difindi  3601  difindir  3602  dif32  3610  csbvarg  3697  undif1  3751  resmpt3  5154  xp0  5253  fresaunres2  5580  fvsnun1  5910  caov12  6290  caov13  6292  caov411  6294  caovdir  6296  orduniss2  6443  fparlem3  6673  fparlem4  6674  hartogslem1  7752  kmlem3  8317  cdaassen  8347  xpcdaen  8348  halfnq  9141  reclem3pr  9214  addcmpblnr  9235  ltsrpr  9240  pn0sr  9264  sqgt0sr  9269  map2psrpr  9273  negsubdii  9689  halfpm6th  10542  i4  11964  nn0opthlem1  12042  fac4  12055  imi  12642  ef01bndlem  13464  bitsres  13665  gcdaddmlem  13708  modsubi  14097  gcdmodi  14099  numexpp1  14103  karatsuba  14109  oppgcntr  15873  frgpuplem  16262  ressmpladd  17526  ressmplmul  17527  ressmplvsca  17528  ltbwe  17542  ressply1add  17639  ressply1mul  17640  ressply1vsca  17641  sn0cld  18594  qtopres  19171  itg1addlem5  21078  cospi  21877  sincos4thpi  21918  sincos3rdpi  21921  dvlog  22039  dvlog2  22041  dvsqr  22125  ang180lem3  22150  1cubrlem  22179  mcubic  22185  quart1lem  22193  atantayl2  22276  log2cnv  22282  log2ublem2  22285  log2ub  22287  chtub  22494  bclbnd  22562  bposlem8  22573  lgsdir2lem1  22605  lgsdir2lem5  22609  ipidsq  24027  ip1ilem  24145  ipdirilem  24148  ipasslem10  24158  siilem1  24170  hvmul2negi  24369  hvadd12i  24378  hvnegdii  24383  normlem1  24431  normlem9  24439  normsubi  24462  normpar2i  24477  polid2i  24478  chjassi  24808  chj12i  24844  pjoml2i  24907  hoadd12i  25100  lnophmlem2  25340  nmopcoadj2i  25425  partfun  25912  archirngz  26123  sqsscirc1  26258  sigaclfu2  26484  eulerpartlemd  26663  coinflippvt  26781  ballotth  26834  gam1  26965  bpoly3  28114  onint1  28209  cnambfre  28349  dvcnsqr  28387  rabren3dioph  29063  arearect  29500  lhe4.4ex1a  29512  expgrowthi  29516  expgrowth  29518  dvcosre  29697  stoweidlem34  29738  bj-csbsn  32115
  Copyright terms: Public domain W3C validator