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  3133  un23  3364  in32  3417  dfrab2  3480  difun2  3572  tpidm23  3770  unisn  3907  dfiunv2  4004  uniop  4346  suc0  4506  unisuc  4508  iunsuc  4515  xpun  4785  dfrn2  4916  dfdmf  4922  dfrnf  4971  res0  5015  resres  5023  xpssres  5046  dfima2  5076  imai  5090  ima0  5093  imaundir  5148  xpima1  5181  xpima2m  5182  dmresv  5193  rescnvcnv  5197  dmtpop  5210  rnsnopg  5213  resdmres  5226  dmmpt  5230  dmco  5243  co01  5249  fpr  5831  fmptpr  5841  fvsnun2  5847  mpo0  6086  dmoprab  6097  rnoprab  6099  ov6g  6155  1st0  6302  2nd0  6303  dfmpo  6383  algrflem  6389  dftpos2  6422  tposoprab  6441  tposmpo  6442  tfrlem8  6479  frecsuc  6568  df2o3  6592  sbthlemi5  7154  sup00  7196  casedm  7279  djudm  7298  axi2m1  8088  2p2e4  9263  numsuc  9617  numsucc  9643  decmul10add  9672  5p5e10  9674  6p4e10  9675  7p3e10  9678  xnegmnf  10057  pnfaddmnf  10078  fz0tp  10350  fz0to3un2pr  10351  fzo0to2pr  10456  fzo0to3tp  10457  fzo0to42pr  10458  0tonninf  10695  1tonninf  10696  inftonninf  10697  sq4e2t8  10892  i4  10897  fac1  10984  fac3  10987  abs0  11612  absi  11613  trirecip  12055  geoihalfsum  12076  esum  12216  tan0  12285  ef01bndlem  12310  3dvds  12418  3dvdsdec  12419  3dvds2dec  12420  3lcm2e6woprm  12651  6lcm4e12  12652  gcdmodi  12987  karatsuba  12996  ennnfonelem1  13021  ndxarg  13098  setsfun  13110  setsfun0  13111  txbasval  14984  cnmpt1st  15005  cnmpt2nd  15006  dvmptidcn  15431  cos2pi  15521  tan4thpi  15558  sincos6thpi  15559  sqrt2cxp2logb9e3  15692  2lgslem3c  15817  2lgslem3d  15818  012of  16542  2o01f  16543  pwf1oexmid  16550  isomninnlem  16584  iswomninnlem  16603  ismkvnnlem  16606