Theorem 3eqtri 2105

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

Syntax hints:   = wceq 1284

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

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

This theorem is referenced by:  csbid  2915  un23  3131  in32  3178  dfrab2  3239  difun2  3322  tpidm23  3493  unisn  3617  dfiunv2  3714  uniop  4010  suc0  4166  unisuc  4168  iunsuc  4175  xpun  4419  dfrn2  4541  dfdmf  4546  dfrnf  4593  res0  4634  resres  4642  xpssres  4663  dfima2  4690  imai  4701  ima0  4704  imaundir  4757  xpima1  4787  xpima2m  4788  dmresv  4799  rescnvcnv  4803  dmtpop  4816  rnsnopg  4819  resdmres  4832  dmmpt  4836  dmco  4849  co01  4855  fpr  5366  fmptpr  5376  fvsnun2  5382  mpt20  5594  dmoprab  5605  rnoprab  5607  ov6g  5658  1st0  5791  2nd0  5792  dfmpt2  5864  algrflem  5870  dftpos2  5899  tposoprab  5918  tposmpt2  5919  tfrlem8  5957  df2o3  6037  sup00  6416  axi2m1  7041  2p2e4  8159  numsuc  8490  numsucc  8516  decmul10add  8545  5p5e10  8547  6p4e10  8548  7p3e10  8551  xnegmnf  8896  fz0tp  9135  fzo0to2pr  9227  fzo0to3tp  9228  fzo0to42pr  9229  i4  9577  fac1  9656  fac3  9659  abs0  9944  absi  9945  3dvdsdec  10264  3dvds2dec  10265  3lcm2e6woprm  10468  6lcm4e12  10469