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

Theorem 3eqtr2i 2309
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 2306 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtri 2303 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  indif  3411  dfrab3  3444  iunid  3957  cnvcnv  5126  cocnvcnv2  5184  fmptap  5710  fpar  6222  fodomr  7012  jech9.3  7486  cda1dif  7802  alephadd  8199  distrnq  8585  ltanq  8595  ltrnq  8603  negdii  9130  halfpm6th  9936  numma  10155  numaddc  10159  6p5lem  10173  binom2i  11212  faclbnd4lem1  11306  0.999...  12337  bitsinv1lem  12632  dfphi2  12842  mod2xnegi  13086  karatsuba  13099  1259lem1  13129  oppgtopn  14826  mgptopn  15334  ply1plusg  16303  ply1vsca  16304  ply1mulr  16305  restcld  16903  cmpsublem  17126  kgentopon  17233  txswaphmeolem  17495  dfii5  18389  itg1climres  19069  ang180lem1  20107  1cubrlem  20137  quart1lem  20151  efiatan  20208  log2cnv  20240  1sgm2ppw  20439  ppiub  20443  bposlem8  20530  bposlem9  20531  ipidsq  21286  ipdirilem  21407  norm3difi  21726  polid2i  21736  pjclem3  22777  cvmdi  22904  ballotth  23096  subfaclim  23719  kur14lem6  23742  ax5seglem7  24563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator