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

Theorem 3eqtr2i 2167
 Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2i.1
3eqtr2i.2
3eqtr2i.3
Assertion
Ref Expression
3eqtr2i

Proof of Theorem 3eqtr2i
StepHypRef Expression
1 3eqtr2i.1 . . 3
2 3eqtr2i.2 . . 3
31, 2eqtr4i 2164 . 2
4 3eqtr2i.3 . 2
53, 4eqtri 2161 1
 Colors of variables: wff set class Syntax hints:   wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  dfrab3  3358  iunid  3877  cnvcnv  5000  cocnvcnv2  5059  fmptap  5619  exmidfodomrlemim  7077  negdii  8090  halfpm6th  8984  numma  9269  numaddc  9273  6p5lem  9295  8p2e10  9305  binom2i  10452  0.999...  11342  flodddiv4  11687  6gcd4e2  11739  dfphi2  11952  txswaphmeolem  12548  cosq23lt0  12982  pigt3  12993  nninfomni  13409
 Copyright terms: Public domain W3C validator