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

Theorem 3eqtr2i 2184
 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 2181 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtri 2178 1 𝐴 = 𝐷
 Colors of variables: wff set class Syntax hints:   = wceq 1335 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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-cleq 2150 This theorem is referenced by:  dfrab3  3383  iunid  3904  cnvcnv  5037  cocnvcnv2  5096  fmptap  5656  exmidfodomrlemim  7130  negdii  8153  halfpm6th  9047  numma  9332  numaddc  9336  6p5lem  9358  8p2e10  9368  binom2i  10520  0.999...  11411  flodddiv4  11817  6gcd4e2  11870  dfphi2  12083  txswaphmeolem  12691  cosq23lt0  13125  pigt3  13136  nninfomni  13562
 Copyright terms: Public domain W3C validator