Theorem 3eqtri 2214

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 2210	. 2 |- B = D
5	1, 4	eqtri 2210	1 |- A = D

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  csbid  3080  un23  3309  in32  3362  dfrab2  3425  difun2  3517  tpidm23  3708  unisn  3840  dfiunv2  3937  uniop  4273  suc0  4429  unisuc  4431  iunsuc  4438  xpun  4705  dfrn2  4833  dfdmf  4838  dfrnf  4886  res0  4929  resres  4937  xpssres  4960  dfima2  4990  imai  5002  ima0  5005  imaundir  5060  xpima1  5093  xpima2m  5094  dmresv  5105  rescnvcnv  5109  dmtpop  5122  rnsnopg  5125  resdmres  5138  dmmpt  5142  dmco  5155  co01  5161  fpr  5719  fmptpr  5729  fvsnun2  5735  mpo0  5966  dmoprab  5977  rnoprab  5979  ov6g  6034  1st0  6169  2nd0  6170  dfmpo  6248  algrflem  6254  dftpos2  6286  tposoprab  6305  tposmpo  6306  tfrlem8  6343  frecsuc  6432  df2o3  6455  sbthlemi5  6990  sup00  7032  casedm  7115  djudm  7134  axi2m1  7904  2p2e4  9076  numsuc  9427  numsucc  9453  decmul10add  9482  5p5e10  9484  6p4e10  9485  7p3e10  9488  xnegmnf  9859  pnfaddmnf  9880  fz0tp  10152  fz0to3un2pr  10153  fzo0to2pr  10248  fzo0to3tp  10249  fzo0to42pr  10250  0tonninf  10470  1tonninf  10471  inftonninf  10472  sq4e2t8  10649  i4  10654  fac1  10741  fac3  10744  abs0  11099  absi  11100  trirecip  11541  geoihalfsum  11562  esum  11702  tan0  11771  ef01bndlem  11796  3dvdsdec  11902  3dvds2dec  11903  3lcm2e6woprm  12118  6lcm4e12  12119  ennnfonelem1  12458  ndxarg  12535  setsfun  12547  setsfun0  12548  txbasval  14224  cnmpt1st  14245  cnmpt2nd  14246  dvmptidcn  14635  cos2pi  14682  tan4thpi  14719  sincos6thpi  14720  sqrt2cxp2logb9e3  14850  012of  15204  2o01f  15205  pwf1oexmid  15208  isomninnlem  15237  iswomninnlem  15256  ismkvnnlem  15259