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

Theorem 3eqtr2i 2322
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 2319 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtri 2316 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  indif  3424  dfrab3  3457  iunid  3973  cnvcnv  5142  cocnvcnv2  5200  fmptap  5726  fpar  6238  fodomr  7028  jech9.3  7502  cda1dif  7818  alephadd  8215  distrnq  8601  ltanq  8611  ltrnq  8619  negdii  9146  halfpm6th  9952  numma  10171  numaddc  10175  6p5lem  10189  binom2i  11228  faclbnd4lem1  11322  0.999...  12353  bitsinv1lem  12648  dfphi2  12858  mod2xnegi  13102  karatsuba  13115  1259lem1  13145  oppgtopn  14842  mgptopn  15350  ply1plusg  16319  ply1vsca  16320  ply1mulr  16321  restcld  16919  cmpsublem  17142  kgentopon  17249  txswaphmeolem  17511  dfii5  18405  itg1climres  19085  ang180lem1  20123  1cubrlem  20153  quart1lem  20167  efiatan  20224  log2cnv  20256  1sgm2ppw  20455  ppiub  20459  bposlem8  20546  bposlem9  20547  ipidsq  21302  ipdirilem  21423  norm3difi  21742  polid2i  21752  pjclem3  22793  cvmdi  22920  ballotth  23112  subfaclim  23734  kur14lem6  23757  ax5seglem7  24635
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