Theorem 3eqtri 2232

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	|- A = B
3eqtri.2	|- B = C
3eqtri.3	|- C = D

Assertion

Ref	Expression
3eqtri	|- A = D

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2228	. 2 |- B = D
5	1, 4	eqtri 2228	1 |- A = D

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 2189

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

This theorem is referenced by:  csbid  3109  un23  3340  in32  3393  dfrab2  3456  difun2  3548  tpidm23  3744  unisn  3880  dfiunv2  3977  uniop  4318  suc0  4476  unisuc  4478  iunsuc  4485  xpun  4754  dfrn2  4884  dfdmf  4890  dfrnf  4938  res0  4982  resres  4990  xpssres  5013  dfima2  5043  imai  5057  ima0  5060  imaundir  5115  xpima1  5148  xpima2m  5149  dmresv  5160  rescnvcnv  5164  dmtpop  5177  rnsnopg  5180  resdmres  5193  dmmpt  5197  dmco  5210  co01  5216  fpr  5789  fmptpr  5799  fvsnun2  5805  mpo0  6038  dmoprab  6049  rnoprab  6051  ov6g  6107  1st0  6253  2nd0  6254  dfmpo  6332  algrflem  6338  dftpos2  6370  tposoprab  6389  tposmpo  6390  tfrlem8  6427  frecsuc  6516  df2o3  6539  sbthlemi5  7089  sup00  7131  casedm  7214  djudm  7233  axi2m1  8023  2p2e4  9198  numsuc  9552  numsucc  9578  decmul10add  9607  5p5e10  9609  6p4e10  9610  7p3e10  9613  xnegmnf  9986  pnfaddmnf  10007  fz0tp  10279  fz0to3un2pr  10280  fzo0to2pr  10384  fzo0to3tp  10385  fzo0to42pr  10386  0tonninf  10622  1tonninf  10623  inftonninf  10624  sq4e2t8  10819  i4  10824  fac1  10911  fac3  10914  abs0  11484  absi  11485  trirecip  11927  geoihalfsum  11948  esum  12088  tan0  12157  ef01bndlem  12182  3dvds  12290  3dvdsdec  12291  3dvds2dec  12292  3lcm2e6woprm  12523  6lcm4e12  12524  gcdmodi  12859  karatsuba  12868  ennnfonelem1  12893  ndxarg  12970  setsfun  12982  setsfun0  12983  txbasval  14854  cnmpt1st  14875  cnmpt2nd  14876  dvmptidcn  15301  cos2pi  15391  tan4thpi  15428  sincos6thpi  15429  sqrt2cxp2logb9e3  15562  2lgslem3c  15687  2lgslem3d  15688  012of  16130  2o01f  16131  pwf1oexmid  16138  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193