Theorem 3eqtri 2231

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  csbid  3105  un23  3336  in32  3389  dfrab2  3452  difun2  3544  tpidm23  3738  unisn  3871  dfiunv2  3968  uniop  4307  suc0  4465  unisuc  4467  iunsuc  4474  xpun  4743  dfrn2  4873  dfdmf  4879  dfrnf  4927  res0  4971  resres  4979  xpssres  5002  dfima2  5032  imai  5046  ima0  5049  imaundir  5104  xpima1  5137  xpima2m  5138  dmresv  5149  rescnvcnv  5153  dmtpop  5166  rnsnopg  5169  resdmres  5182  dmmpt  5186  dmco  5199  co01  5205  fpr  5778  fmptpr  5788  fvsnun2  5794  mpo0  6027  dmoprab  6038  rnoprab  6040  ov6g  6096  1st0  6242  2nd0  6243  dfmpo  6321  algrflem  6327  dftpos2  6359  tposoprab  6378  tposmpo  6379  tfrlem8  6416  frecsuc  6505  df2o3  6528  sbthlemi5  7077  sup00  7119  casedm  7202  djudm  7221  axi2m1  8003  2p2e4  9178  numsuc  9532  numsucc  9558  decmul10add  9587  5p5e10  9589  6p4e10  9590  7p3e10  9593  xnegmnf  9966  pnfaddmnf  9987  fz0tp  10259  fz0to3un2pr  10260  fzo0to2pr  10364  fzo0to3tp  10365  fzo0to42pr  10366  0tonninf  10602  1tonninf  10603  inftonninf  10604  sq4e2t8  10799  i4  10804  fac1  10891  fac3  10894  abs0  11439  absi  11440  trirecip  11882  geoihalfsum  11903  esum  12043  tan0  12112  ef01bndlem  12137  3dvds  12245  3dvdsdec  12246  3dvds2dec  12247  3lcm2e6woprm  12478  6lcm4e12  12479  gcdmodi  12814  karatsuba  12823  ennnfonelem1  12848  ndxarg  12925  setsfun  12937  setsfun0  12938  txbasval  14809  cnmpt1st  14830  cnmpt2nd  14831  dvmptidcn  15256  cos2pi  15346  tan4thpi  15383  sincos6thpi  15384  sqrt2cxp2logb9e3  15517  2lgslem3c  15642  2lgslem3d  15643  012of  16065  2o01f  16066  pwf1oexmid  16071  isomninnlem  16104  iswomninnlem  16123  ismkvnnlem  16126