Theorem 3eqtr2i 2204

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

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 |- A = B
2		3eqtr2i.2	. . 3 |- C = B
3	1, 2	eqtr4i 2201	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2198	1 |- A = D

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  3413  iunid  3944  cnvcnv  5083  cocnvcnv2  5142  fmptap  5709  exmidfodomrlemim  7203  negdii  8244  halfpm6th  9142  numma  9430  numaddc  9434  6p5lem  9456  8p2e10  9466  binom2i  10632  0.999...  11532  flodddiv4  11942  6gcd4e2  11999  dfphi2  12223  txswaphmeolem  13960  cosq23lt0  14394  pigt3  14405  2lgsoddprmlem3c  14597  2lgsoddprmlem3d  14598  nninfomni  14909