Theorem 3eqtri 2195

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 2191	. 2 |- B = D
5	1, 4	eqtri 2191	1 |- A = D

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  csbid  3057  un23  3286  in32  3339  dfrab2  3402  difun2  3493  tpidm23  3682  unisn  3810  dfiunv2  3907  uniop  4238  suc0  4394  unisuc  4396  iunsuc  4403  xpun  4670  dfrn2  4797  dfdmf  4802  dfrnf  4850  res0  4893  resres  4901  xpssres  4924  dfima2  4953  imai  4965  ima0  4968  imaundir  5022  xpima1  5055  xpima2m  5056  dmresv  5067  rescnvcnv  5071  dmtpop  5084  rnsnopg  5087  resdmres  5100  dmmpt  5104  dmco  5117  co01  5123  fpr  5676  fmptpr  5686  fvsnun2  5692  mpo0  5921  dmoprab  5932  rnoprab  5934  ov6g  5988  1st0  6121  2nd0  6122  dfmpo  6200  algrflem  6206  dftpos2  6238  tposoprab  6257  tposmpo  6258  tfrlem8  6295  frecsuc  6384  df2o3  6407  sbthlemi5  6936  sup00  6978  casedm  7061  djudm  7080  axi2m1  7830  2p2e4  8998  numsuc  9349  numsucc  9375  decmul10add  9404  5p5e10  9406  6p4e10  9407  7p3e10  9410  xnegmnf  9779  pnfaddmnf  9800  fz0tp  10071  fz0to3un2pr  10072  fzo0to2pr  10167  fzo0to3tp  10168  fzo0to42pr  10169  0tonninf  10388  1tonninf  10389  inftonninf  10390  sq4e2t8  10566  i4  10571  fac1  10656  fac3  10659  abs0  11015  absi  11016  trirecip  11457  geoihalfsum  11478  esum  11618  tan0  11687  ef01bndlem  11712  3dvdsdec  11817  3dvds2dec  11818  3lcm2e6woprm  12033  6lcm4e12  12034  ennnfonelem1  12355  ndxarg  12432  setsfun  12444  setsfun0  12445  txbasval  13026  cnmpt1st  13047  cnmpt2nd  13048  dvmptidcn  13437  cos2pi  13484  tan4thpi  13521  sincos6thpi  13522  sqrt2cxp2logb9e3  13652  012of  13993  2o01f  13994  pwf1oexmid  13997  isomninnlem  14027  iswomninnlem  14046  ismkvnnlem  14049