Theorem 3eqtri 2257

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	⊢ 𝐴 = 𝐵
3eqtri.2	⊢ 𝐵 = 𝐶
3eqtri.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtri	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3		3eqtri.3	. . 3 ⊢ 𝐶 = 𝐷
4	2, 3	eqtri 2253	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2253	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225

This theorem is referenced by:  csbid  3145  un23  3377  in32  3432  dfrab2  3495  difun2  3588  if0ab  3622  tpidm23  3791  unisn  3929  dfiunv2  4026  uniop  4371  suc0  4531  unisuc  4533  iunsuc  4540  xpun  4810  dfrn2  4942  dfdmf  4948  dfrnf  4997  res0  5041  resres  5049  xpssres  5072  dfima2  5102  imai  5117  ima0  5120  imaundir  5175  xpima1  5208  xpima2m  5209  dmresv  5220  rescnvcnv  5224  dmtpop  5237  rnsnopg  5240  resdmres  5253  dmmpt  5257  dmco  5270  co01  5276  fpr  5865  fmptpr  5875  fvsnun2  5881  mpo0  6122  dmoprab  6133  rnoprab  6135  ov6g  6191  1st0  6337  2nd0  6338  dfmpo  6418  algrflem  6424  dftpos2  6491  tposoprab  6510  tposmpo  6511  tfrlem8  6548  frecsuc  6637  df2o3  6661  sbthlemi5  7230  sup00  7293  casedm  7376  djudm  7395  axi2m1  8189  2p2e4  9363  numsuc  9721  numsucc  9747  decmul10add  9776  5p5e10  9778  6p4e10  9779  7p3e10  9782  xnegmnf  10161  pnfaddmnf  10182  fz0tp  10455  fz0to3un2pr  10456  fzo0to2pr  10562  fzo0to3tp  10563  fzo0to42pr  10564  0tonninf  10801  1tonninf  10802  inftonninf  10803  sq4e2t8  10998  i4  11003  fac1  11090  fac3  11093  abs0  11739  absi  11740  trirecip  12183  geoihalfsum  12204  esum  12344  tan0  12413  ef01bndlem  12438  3dvds  12546  3dvdsdec  12547  3dvds2dec  12548  3lcm2e6woprm  12779  6lcm4e12  12780  gcdmodi  13115  karatsuba  13124  ennnfonelem1  13150  ndxarg  13227  setsfun  13239  setsfun0  13240  txbasval  15124  cnmpt1st  15145  cnmpt2nd  15146  dvmptidcn  15571  cos2pi  15661  tan4thpi  15698  sincos6thpi  15699  sqrt2cxp2logb9e3  15832  2lgslem3c  15960  2lgslem3d  15961  012of  16759  2o01f  16760  pwf1oexmid  16765  isomninnlem  16806  iswomninnlem  16826  ismkvnnlem  16829