Theorem 3eqtri 2202

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	|- A = B
3eqtri.2	|- B = C
3eqtri.3	|- C = D

Assertion

Ref	Expression
3eqtri	|- A = D

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2198	. 2 |- B = D
5	1, 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:  csbid  3066  un23  3295  in32  3348  dfrab2  3411  difun2  3503  tpidm23  3694  unisn  3826  dfiunv2  3923  uniop  4256  suc0  4412  unisuc  4414  iunsuc  4421  xpun  4688  dfrn2  4816  dfdmf  4821  dfrnf  4869  res0  4912  resres  4920  xpssres  4943  dfima2  4973  imai  4985  ima0  4988  imaundir  5043  xpima1  5076  xpima2m  5077  dmresv  5088  rescnvcnv  5092  dmtpop  5105  rnsnopg  5108  resdmres  5121  dmmpt  5125  dmco  5138  co01  5144  fpr  5699  fmptpr  5709  fvsnun2  5715  mpo0  5945  dmoprab  5956  rnoprab  5958  ov6g  6012  1st0  6145  2nd0  6146  dfmpo  6224  algrflem  6230  dftpos2  6262  tposoprab  6281  tposmpo  6282  tfrlem8  6319  frecsuc  6408  df2o3  6431  sbthlemi5  6960  sup00  7002  casedm  7085  djudm  7104  axi2m1  7874  2p2e4  9046  numsuc  9397  numsucc  9423  decmul10add  9452  5p5e10  9454  6p4e10  9455  7p3e10  9458  xnegmnf  9829  pnfaddmnf  9850  fz0tp  10122  fz0to3un2pr  10123  fzo0to2pr  10218  fzo0to3tp  10219  fzo0to42pr  10220  0tonninf  10439  1tonninf  10440  inftonninf  10441  sq4e2t8  10618  i4  10623  fac1  10709  fac3  10712  abs0  11067  absi  11068  trirecip  11509  geoihalfsum  11530  esum  11670  tan0  11739  ef01bndlem  11764  3dvdsdec  11870  3dvds2dec  11871  3lcm2e6woprm  12086  6lcm4e12  12087  ennnfonelem1  12408  ndxarg  12485  setsfun  12497  setsfun0  12498  txbasval  13770  cnmpt1st  13791  cnmpt2nd  13792  dvmptidcn  14181  cos2pi  14228  tan4thpi  14265  sincos6thpi  14266  sqrt2cxp2logb9e3  14396  012of  14748  2o01f  14749  pwf1oexmid  14752  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803