Theorem 3eqtri 2254

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbid  3132  un23  3363  in32  3416  dfrab2  3479  difun2  3571  tpidm23  3767  unisn  3903  dfiunv2  4000  uniop  4341  suc0  4501  unisuc  4503  iunsuc  4510  xpun  4779  dfrn2  4909  dfdmf  4915  dfrnf  4964  res0  5008  resres  5016  xpssres  5039  dfima2  5069  imai  5083  ima0  5086  imaundir  5141  xpima1  5174  xpima2m  5175  dmresv  5186  rescnvcnv  5190  dmtpop  5203  rnsnopg  5206  resdmres  5219  dmmpt  5223  dmco  5236  co01  5242  fpr  5820  fmptpr  5830  fvsnun2  5836  mpo0  6073  dmoprab  6084  rnoprab  6086  ov6g  6142  1st0  6288  2nd0  6289  dfmpo  6367  algrflem  6373  dftpos2  6405  tposoprab  6424  tposmpo  6425  tfrlem8  6462  frecsuc  6551  df2o3  6574  sbthlemi5  7124  sup00  7166  casedm  7249  djudm  7268  axi2m1  8058  2p2e4  9233  numsuc  9587  numsucc  9613  decmul10add  9642  5p5e10  9644  6p4e10  9645  7p3e10  9648  xnegmnf  10021  pnfaddmnf  10042  fz0tp  10314  fz0to3un2pr  10315  fzo0to2pr  10419  fzo0to3tp  10420  fzo0to42pr  10421  0tonninf  10657  1tonninf  10658  inftonninf  10659  sq4e2t8  10854  i4  10859  fac1  10946  fac3  10949  abs0  11564  absi  11565  trirecip  12007  geoihalfsum  12028  esum  12168  tan0  12237  ef01bndlem  12262  3dvds  12370  3dvdsdec  12371  3dvds2dec  12372  3lcm2e6woprm  12603  6lcm4e12  12604  gcdmodi  12939  karatsuba  12948  ennnfonelem1  12973  ndxarg  13050  setsfun  13062  setsfun0  13063  txbasval  14935  cnmpt1st  14956  cnmpt2nd  14957  dvmptidcn  15382  cos2pi  15472  tan4thpi  15509  sincos6thpi  15510  sqrt2cxp2logb9e3  15643  2lgslem3c  15768  2lgslem3d  15769  012of  16316  2o01f  16317  pwf1oexmid  16324  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379