Theorem 3eqtri 2218

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

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  csbid  3089  un23  3319  in32  3372  dfrab2  3435  difun2  3527  tpidm23  3720  unisn  3852  dfiunv2  3949  uniop  4285  suc0  4443  unisuc  4445  iunsuc  4452  xpun  4721  dfrn2  4851  dfdmf  4856  dfrnf  4904  res0  4947  resres  4955  xpssres  4978  dfima2  5008  imai  5022  ima0  5025  imaundir  5080  xpima1  5113  xpima2m  5114  dmresv  5125  rescnvcnv  5129  dmtpop  5142  rnsnopg  5145  resdmres  5158  dmmpt  5162  dmco  5175  co01  5181  fpr  5741  fmptpr  5751  fvsnun2  5757  mpo0  5989  dmoprab  6000  rnoprab  6002  ov6g  6058  1st0  6199  2nd0  6200  dfmpo  6278  algrflem  6284  dftpos2  6316  tposoprab  6335  tposmpo  6336  tfrlem8  6373  frecsuc  6462  df2o3  6485  sbthlemi5  7022  sup00  7064  casedm  7147  djudm  7166  axi2m1  7937  2p2e4  9111  numsuc  9464  numsucc  9490  decmul10add  9519  5p5e10  9521  6p4e10  9522  7p3e10  9525  xnegmnf  9898  pnfaddmnf  9919  fz0tp  10191  fz0to3un2pr  10192  fzo0to2pr  10288  fzo0to3tp  10289  fzo0to42pr  10290  0tonninf  10514  1tonninf  10515  inftonninf  10516  sq4e2t8  10711  i4  10716  fac1  10803  fac3  10806  abs0  11205  absi  11206  trirecip  11647  geoihalfsum  11668  esum  11808  tan0  11877  ef01bndlem  11902  3dvdsdec  12009  3dvds2dec  12010  3lcm2e6woprm  12227  6lcm4e12  12228  ennnfonelem1  12567  ndxarg  12644  setsfun  12656  setsfun0  12657  txbasval  14446  cnmpt1st  14467  cnmpt2nd  14468  dvmptidcn  14893  cos2pi  14980  tan4thpi  15017  sincos6thpi  15018  sqrt2cxp2logb9e3  15148  2lgslem3c  15252  2lgslem3d  15253  012of  15556  2o01f  15557  pwf1oexmid  15560  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612