Theorem 3eqtri 2109

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

Syntax hints:   = wceq 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078

This theorem is referenced by:  csbid  2929  un23  3148  in32  3201  dfrab2  3263  difun2  3349  tpidm23  3526  unisn  3652  dfiunv2  3749  uniop  4056  suc0  4212  unisuc  4214  iunsuc  4221  xpun  4467  dfrn2  4592  dfdmf  4597  dfrnf  4644  res0  4685  resres  4693  xpssres  4714  dfima2  4743  imai  4755  ima0  4758  imaundir  4811  xpima1  4843  xpima2m  4844  dmresv  4855  rescnvcnv  4859  dmtpop  4872  rnsnopg  4875  resdmres  4888  dmmpt  4892  dmco  4905  co01  4911  fpr  5442  fmptpr  5452  fvsnun2  5458  mpt20  5675  dmoprab  5686  rnoprab  5688  ov6g  5739  1st0  5872  2nd0  5873  dfmpt2  5945  algrflem  5951  dftpos2  5980  tposoprab  5999  tposmpt2  6000  tfrlem8  6037  frecsuc  6126  df2o3  6149  sbthlemi5  6614  sup00  6642  casedm  6721  djudm  6729  axi2m1  7354  2p2e4  8477  numsuc  8822  numsucc  8848  decmul10add  8877  5p5e10  8879  6p4e10  8880  7p3e10  8883  xnegmnf  9223  fz0tp  9463  fzo0to2pr  9557  fzo0to3tp  9558  fzo0to42pr  9559  0tonninf  9773  1tonninf  9774  inftonninf  9775  i4  9954  fac1  10033  fac3  10036  abs0  10386  absi  10387  3dvdsdec  10740  3dvds2dec  10741  3lcm2e6woprm  10943  6lcm4e12  10944