Theorem 3eqtri 2256

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 2252	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2252	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  csbid  3135  un23  3366  in32  3419  dfrab2  3482  difun2  3574  tpidm23  3772  unisn  3909  dfiunv2  4006  uniop  4348  suc0  4508  unisuc  4510  iunsuc  4517  xpun  4787  dfrn2  4918  dfdmf  4924  dfrnf  4973  res0  5017  resres  5025  xpssres  5048  dfima2  5078  imai  5092  ima0  5095  imaundir  5150  xpima1  5183  xpima2m  5184  dmresv  5195  rescnvcnv  5199  dmtpop  5212  rnsnopg  5215  resdmres  5228  dmmpt  5232  dmco  5245  co01  5251  fpr  5836  fmptpr  5846  fvsnun2  5852  mpo0  6091  dmoprab  6102  rnoprab  6104  ov6g  6160  1st0  6307  2nd0  6308  dfmpo  6388  algrflem  6394  dftpos2  6427  tposoprab  6446  tposmpo  6447  tfrlem8  6484  frecsuc  6573  df2o3  6597  sbthlemi5  7160  sup00  7202  casedm  7285  djudm  7304  axi2m1  8095  2p2e4  9270  numsuc  9624  numsucc  9650  decmul10add  9679  5p5e10  9681  6p4e10  9682  7p3e10  9685  xnegmnf  10064  pnfaddmnf  10085  fz0tp  10357  fz0to3un2pr  10358  fzo0to2pr  10464  fzo0to3tp  10465  fzo0to42pr  10466  0tonninf  10703  1tonninf  10704  inftonninf  10705  sq4e2t8  10900  i4  10905  fac1  10992  fac3  10995  abs0  11623  absi  11624  trirecip  12067  geoihalfsum  12088  esum  12228  tan0  12297  ef01bndlem  12322  3dvds  12430  3dvdsdec  12431  3dvds2dec  12432  3lcm2e6woprm  12663  6lcm4e12  12664  gcdmodi  12999  karatsuba  13008  ennnfonelem1  13033  ndxarg  13110  setsfun  13122  setsfun0  13123  txbasval  14997  cnmpt1st  15018  cnmpt2nd  15019  dvmptidcn  15444  cos2pi  15534  tan4thpi  15571  sincos6thpi  15572  sqrt2cxp2logb9e3  15705  2lgslem3c  15830  2lgslem3d  15831  012of  16618  2o01f  16619  pwf1oexmid  16626  isomninnlem  16660  iswomninnlem  16679  ismkvnnlem  16682