ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr2i Unicode version

Theorem 3eqtr2i 2192
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 2189 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtri 2186 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-cleq 2158
This theorem is referenced by:  dfrab3  3398  iunid  3921  cnvcnv  5056  cocnvcnv2  5115  fmptap  5675  exmidfodomrlemim  7157  negdii  8182  halfpm6th  9077  numma  9365  numaddc  9369  6p5lem  9391  8p2e10  9401  binom2i  10563  0.999...  11462  flodddiv4  11871  6gcd4e2  11928  dfphi2  12152  txswaphmeolem  12960  cosq23lt0  13394  pigt3  13405  nninfomni  13899
  Copyright terms: Public domain W3C validator