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  3904  dfiunv2  4001  uniop  4342  suc0  4502  unisuc  4504  iunsuc  4511  xpun  4780  dfrn2  4910  dfdmf  4916  dfrnf  4965  res0  5009  resres  5017  xpssres  5040  dfima2  5070  imai  5084  ima0  5087  imaundir  5142  xpima1  5175  xpima2m  5176  dmresv  5187  rescnvcnv  5191  dmtpop  5204  rnsnopg  5207  resdmres  5220  dmmpt  5224  dmco  5237  co01  5243  fpr  5825  fmptpr  5835  fvsnun2  5841  mpo0  6080  dmoprab  6091  rnoprab  6093  ov6g  6149  1st0  6296  2nd0  6297  dfmpo  6375  algrflem  6381  dftpos2  6413  tposoprab  6432  tposmpo  6433  tfrlem8  6470  frecsuc  6559  df2o3  6583  sbthlemi5  7136  sup00  7178  casedm  7261  djudm  7280  axi2m1  8070  2p2e4  9245  numsuc  9599  numsucc  9625  decmul10add  9654  5p5e10  9656  6p4e10  9657  7p3e10  9660  xnegmnf  10033  pnfaddmnf  10054  fz0tp  10326  fz0to3un2pr  10327  fzo0to2pr  10432  fzo0to3tp  10433  fzo0to42pr  10434  0tonninf  10670  1tonninf  10671  inftonninf  10672  sq4e2t8  10867  i4  10872  fac1  10959  fac3  10962  abs0  11577  absi  11578  trirecip  12020  geoihalfsum  12041  esum  12181  tan0  12250  ef01bndlem  12275  3dvds  12383  3dvdsdec  12384  3dvds2dec  12385  3lcm2e6woprm  12616  6lcm4e12  12617  gcdmodi  12952  karatsuba  12961  ennnfonelem1  12986  ndxarg  13063  setsfun  13075  setsfun0  13076  txbasval  14949  cnmpt1st  14970  cnmpt2nd  14971  dvmptidcn  15396  cos2pi  15486  tan4thpi  15523  sincos6thpi  15524  sqrt2cxp2logb9e3  15657  2lgslem3c  15782  2lgslem3d  15783  012of  16386  2o01f  16387  pwf1oexmid  16394  isomninnlem  16428  iswomninnlem  16447  ismkvnnlem  16450