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

Theorem 3eqtr2i 2502
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2i.1  |-  A  =  B
3eqtr2i.2  |-  C  =  B
3eqtr2i.3  |-  C  =  D
Assertion
Ref Expression
3eqtr2i  |-  A  =  D

Proof of Theorem 3eqtr2i
StepHypRef Expression
1 3eqtr2i.1 . . 3  |-  A  =  B
2 3eqtr2i.2 . . 3  |-  C  =  B
31, 2eqtr4i 2499 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtri 2496 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  indif  3740  dfrab3  3773  iunid  4380  cnvcnv  5459  cocnvcnv2  5519  fmptap  6085  fpar  6888  fodomr  7669  jech9.3  8233  cda1dif  8557  alephadd  8953  distrnq  9340  ltanq  9350  ltrnq  9358  negdii  9904  halfpm6th  10761  numma  11008  numaddc  11012  6p5lem  11026  binom2i  12246  faclbnd4lem1  12340  0.999...  13656  dfphi2  14166  mod2xnegi  14419  karatsuba  14432  1259lem1  14474  oppgtopn  16202  mgptopn  16964  ply1plusg  18077  ply1vsca  18078  ply1mulr  18079  restcld  19479  cmpsublem  19705  kgentopon  19866  txswaphmeolem  20132  dfii5  21216  itg1climres  21948  efsubm  22763  ang180lem1  22966  1cubrlem  22997  quart1lem  23011  efiatan  23068  log2cnv  23100  1sgm2ppw  23300  ppiub  23304  bposlem8  23391  bposlem9  23392  ax5seglem7  24011  usgraexmplcvtx  24178  usgraexmplcedg  24179  ipidsq  25396  ipdirilem  25517  norm3difi  25837  polid2i  25847  pjclem3  26889  cvmdi  27016  eulerpartlemt  28061  ballotlem1  28176  ballotlemfval0  28185  ballotth  28227  subfaclim  28383  kur14lem6  28406  volsupnfl  29912  areaquad  31016  wallispilem4  31595  zlmodzxz0  32240  linevalexample  32294
  Copyright terms: Public domain W3C validator