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  4396  suc0  4556  unisuc  4558  iunsuc  4565  xpun  4836  dfrn2  4968  dfdmf  4974  dfrnf  5023  res0  5067  resres  5075  xpssres  5098  dfima2  5128  imai  5143  ima0  5146  imaundir  5201  xpima1  5234  xpima2m  5235  dmresv  5246  rescnvcnv  5250  dmtpop  5263  rnsnopg  5266  resdmres  5279  dmmpt  5283  dmco  5296  co01  5302  fpr  5897  fmptpr  5907  fvsnun2  5913  mpo0  6158  dmoprab  6169  rnoprab  6171  ov6g  6227  1st0  6378  2nd0  6379  dfmpo  6459  algrflem  6465  dftpos2  6532  tposoprab  6551  tposmpo  6552  tfrlem8  6589  frecsuc  6678  df2o3  6702  sbthlemi5  7278  sup00  7343  casedm  7426  djudm  7445  axi2m1  8242  2p2e4  9433  numsuc  9794  numsucc  9825  decmul10add  9854  5p5e10  9856  6p4e10  9857  7p3e10  9860  xnegmnf  10241  pnfaddmnf  10262  fz0tp  10539  fz0to3un2pr  10540  fzo0to2pr  10646  fzo0to3tp  10647  fzo0to42pr  10648  0tonninf  10890  1tonninf  10891  inftonninf  10892  sq4e2t8  11087  i4  11092  fac1  11181  fac3  11184  abs0  11838  absi  11839  trirecip  12284  geoihalfsum  12305  esum  12445  tan0  12514  ef01bndlem  12539  3dvds  12647  3dvdsdec  12648  3dvds2dec  12649  3lcm2e6woprm  12880  6lcm4e12  12881  gcdmodi  13221  karatsuba  13230  43prm  13256  139prm  13258  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  ballotfilem2  13277  ballotfilemth  13330  ennnfonelem1  13347  ndxarg  13424  setsfun  13436  setsfun0  13437  txbasval  15417  cnmpt1st  15438  cnmpt2nd  15439  dvmptidcn  15864  cos2pi  15955  tan4thpi  15992  sincos6thpi  15993  sqrt2cxp2logb9e3  16130  log2ublem2  16141  log2ublem3  16142  birthdaylog2  16147  ppi1i  16177  ppi2i  16178  bclbnd  16205  2lgslem3c  16312  2lgslem3d  16313  012of  17121  2o01f  17122  pwf1oexmid  17127  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200