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

Theorem 3eqtr2i 2463
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 2460 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtri 2457 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1653
This theorem is referenced by:  indif  3584  dfrab3  3618  iunid  4147  cnvcnv  5324  cocnvcnv2  5382  fmptap  5924  fpar  6451  fodomr  7259  jech9.3  7741  cda1dif  8057  alephadd  8453  distrnq  8839  ltanq  8849  ltrnq  8857  negdii  9385  halfpm6th  10193  numma  10414  numaddc  10418  6p5lem  10432  binom2i  11491  faclbnd4lem1  11585  0.999...  12659  dfphi2  13164  mod2xnegi  13408  karatsuba  13421  1259lem1  13451  oppgtopn  15150  mgptopn  15658  ply1plusg  16620  ply1vsca  16621  ply1mulr  16622  restcld  17237  cmpsublem  17463  kgentopon  17571  txswaphmeolem  17837  dfii5  18916  itg1climres  19607  ang180lem1  20652  1cubrlem  20682  quart1lem  20696  efiatan  20753  log2cnv  20785  1sgm2ppw  20985  ppiub  20989  bposlem8  21076  bposlem9  21077  ipidsq  22210  ipdirilem  22331  norm3difi  22650  polid2i  22660  pjclem3  23701  cvmdi  23828  ballotlem1  24745  ballotlemfval0  24754  ballotth  24796  subfaclim  24875  kur14lem6  24898  ax5seglem7  25875  volsupnfl  26252  wallispilem4  27794
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 2418
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2430
  Copyright terms: Public domain W3C validator