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  6537  tposoprab  6556  tposmpo  6557  tfrlem8  6594  frecsuc  6683  df2o3  6707  sbthlemi5  7285  sup00  7349  casedm  7432  djudm  7451  axi2m1  8248  2p2e4  9440  numsuc  9800  numsucc  9831  decmul10add  9860  5p5e10  9862  6p4e10  9863  7p3e10  9866  xnegmnf  10247  pnfaddmnf  10268  fz0tp  10545  fz0to3un2pr  10546  fzo0to2pr  10652  fzo0to3tp  10653  fzo0to42pr  10654  0tonninf  10897  1tonninf  10898  inftonninf  10899  sq4e2t8  11094  i4  11099  fac1  11188  fac3  11191  abs0  11845  absi  11846  trirecip  12292  geoihalfsum  12313  esum  12453  tan0  12522  ef01bndlem  12547  3dvds  12655  3dvdsdec  12656  3dvds2dec  12657  3lcm2e6woprm  12888  6lcm4e12  12889  gcdmodi  13229  karatsuba  13238  43prm  13264  139prm  13266  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  ballotfilem2  13285  ballotfilemth  13338  ennnfonelem1  13355  ndxarg  13432  setsfun  13444  setsfun0  13445  txbasval  15510  cnmpt1st  15531  cnmpt2nd  15532  dvmptidcn  15957  cos2pi  16048  tan4thpi  16085  sincos6thpi  16086  sqrt2cxp2logb9e3  16228  log2ublem2  16239  log2ublem3  16240  birthdaylog2  16245  cht1  16288  ppi1i  16289  ppi2i  16290  cht2  16293  cht3  16294  bclbnd  16324  bposlem8  16335  2lgslem3c  16436  2lgslem3d  16437  012of  17245  2o01f  17246  pwf1oexmid  17251  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326