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

Theorem 3eqtr2i 2204
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 2201 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtri 2198 1 𝐴 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  dfrab3  3411  iunid  3941  cnvcnv  5080  cocnvcnv2  5139  fmptap  5705  exmidfodomrlemim  7197  negdii  8237  halfpm6th  9135  numma  9423  numaddc  9427  6p5lem  9449  8p2e10  9459  binom2i  10623  0.999...  11522  flodddiv4  11931  6gcd4e2  11988  dfphi2  12212  txswaphmeolem  13691  cosq23lt0  14125  pigt3  14136  nninfomni  14628
  Copyright terms: Public domain W3C validator