Theorem 3eqtri 2263

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbid  3155  un23  3388  in32  3443  dfrab2  3508  dfnul4  3522  difun2  3607  if0ab  3641  tpidm23  3812  unisn  3951  dfiunv2  4048  uniop  4398  suc0  4558  unisuc  4560  iunsuc  4567  xpun  4838  dfrn2  4970  dfdmf  4976  dfrnf  5025  res0  5069  resres  5077  xpssres  5100  dfima2  5131  imai  5146  ima0  5149  imaundir  5204  xpima1  5237  xpima2m  5238  dmresv  5249  rescnvcnv  5253  dmtpop  5266  rnsnopg  5269  resdmres  5282  dmmpt  5286  dmco  5299  co01  5305  fpr  5900  fmptpr  5910  fvsnun2  5916  mpo0  6161  dmoprab  6172  rnoprab  6174  ov6g  6230  1st0  6382  2nd0  6383  dfmpo  6463  algrflem  6469  dftpos2  6536  tposoprab  6555  tposmpo  6556  tfrlem8  6593  frecsuc  6682  df2o3  6706  sbthlemi5  7283  sup00  7349  casedm  7432  djudm  7451  axi2m1  8248  2p2e4  9440  numsuc  9801  numsucc  9832  decmul10add  9861  5p5e10  9863  6p4e10  9864  7p3e10  9867  xnegmnf  10248  pnfaddmnf  10269  fz0tp  10546  fz0to3un2pr  10547  fzo0to2pr  10653  fzo0to3tp  10654  fzo0to42pr  10655  0tonninf  10898  1tonninf  10899  inftonninf  10900  sq4e2t8  11095  i4  11100  fac1  11189  fac3  11192  abs0  11846  absi  11847  trirecip  12293  geoihalfsum  12314  esum  12454  tan0  12523  ef01bndlem  12548  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  3lcm2e6woprm  12889  6lcm4e12  12890  gcdmodi  13230  karatsuba  13239  43prm  13265  139prm  13267  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  ballotfilem2  13286  ballotfilemth  13339  ennnfonelem1  13356  ndxarg  13433  setsfun  13445  setsfun0  13446  txbasval  15493  cnmpt1st  15514  cnmpt2nd  15515  dvmptidcn  15940  cos2pi  16031  tan4thpi  16068  sincos6thpi  16069  sqrt2cxp2logb9e3  16211  log2ublem2  16222  log2ublem3  16223  birthdaylog2  16228  cht1  16271  ppi1i  16272  ppi2i  16273  cht2  16276  cht3  16277  bclbnd  16307  bposlem8  16318  2lgslem3c  16419  2lgslem3d  16420  012of  17228  2o01f  17229  pwf1oexmid  17234  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309