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  9431  numsuc  9790  numsucc  9816  decmul10add  9845  5p5e10  9847  6p4e10  9848  7p3e10  9851  xnegmnf  10231  pnfaddmnf  10252  fz0tp  10529  fz0to3un2pr  10530  fzo0to2pr  10636  fzo0to3tp  10637  fzo0to42pr  10638  0tonninf  10877  1tonninf  10878  inftonninf  10879  sq4e2t8  11074  i4  11079  fac1  11167  fac3  11170  abs0  11824  absi  11825  trirecip  12268  geoihalfsum  12289  esum  12429  tan0  12498  ef01bndlem  12523  3dvds  12631  3dvdsdec  12632  3dvds2dec  12633  3lcm2e6woprm  12864  6lcm4e12  12865  gcdmodi  13200  karatsuba  13209  ballotfilem2  13228  ballotfilemth  13281  ennnfonelem1  13298  ndxarg  13375  setsfun  13387  setsfun0  13388  txbasval  15368  cnmpt1st  15389  cnmpt2nd  15390  dvmptidcn  15815  cos2pi  15905  tan4thpi  15942  sincos6thpi  15943  sqrt2cxp2logb9e3  16077  log2ublem2  16084  log2ublem3  16085  birthdaylog2  16090  2lgslem3c  16214  2lgslem3d  16215  012of  17023  2o01f  17024  pwf1oexmid  17029  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102