Theorem 3eqtri 2190

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  csbid  3052  un23  3280  in32  3333  dfrab2  3396  difun2  3487  tpidm23  3676  unisn  3804  dfiunv2  3901  uniop  4232  suc0  4388  unisuc  4390  iunsuc  4397  xpun  4664  dfrn2  4791  dfdmf  4796  dfrnf  4844  res0  4887  resres  4895  xpssres  4918  dfima2  4947  imai  4959  ima0  4962  imaundir  5016  xpima1  5049  xpima2m  5050  dmresv  5061  rescnvcnv  5065  dmtpop  5078  rnsnopg  5081  resdmres  5094  dmmpt  5098  dmco  5111  co01  5117  fpr  5666  fmptpr  5676  fvsnun2  5682  mpo0  5908  dmoprab  5919  rnoprab  5921  ov6g  5975  1st0  6109  2nd0  6110  dfmpo  6187  algrflem  6193  dftpos2  6225  tposoprab  6244  tposmpo  6245  tfrlem8  6282  frecsuc  6371  df2o3  6394  sbthlemi5  6922  sup00  6964  casedm  7047  djudm  7066  axi2m1  7812  2p2e4  8980  numsuc  9331  numsucc  9357  decmul10add  9386  5p5e10  9388  6p4e10  9389  7p3e10  9392  xnegmnf  9761  pnfaddmnf  9782  fz0tp  10053  fz0to3un2pr  10054  fzo0to2pr  10149  fzo0to3tp  10150  fzo0to42pr  10151  0tonninf  10370  1tonninf  10371  inftonninf  10372  sq4e2t8  10548  i4  10553  fac1  10638  fac3  10641  abs0  10996  absi  10997  trirecip  11438  geoihalfsum  11459  esum  11599  tan0  11668  ef01bndlem  11693  3dvdsdec  11798  3dvds2dec  11799  3lcm2e6woprm  12014  6lcm4e12  12015  ennnfonelem1  12336  ndxarg  12413  setsfun  12425  setsfun0  12426  txbasval  12867  cnmpt1st  12888  cnmpt2nd  12889  dvmptidcn  13278  cos2pi  13325  tan4thpi  13362  sincos6thpi  13363  sqrt2cxp2logb9e3  13493  012of  13835  2o01f  13836  pwf1oexmid  13839  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891