Theorem 3eqtri 2202

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  csbid  3067  un23  3296  in32  3349  dfrab2  3412  difun2  3504  tpidm23  3695  unisn  3827  dfiunv2  3924  uniop  4257  suc0  4413  unisuc  4415  iunsuc  4422  xpun  4689  dfrn2  4817  dfdmf  4822  dfrnf  4870  res0  4913  resres  4921  xpssres  4944  dfima2  4974  imai  4986  ima0  4989  imaundir  5044  xpima1  5077  xpima2m  5078  dmresv  5089  rescnvcnv  5093  dmtpop  5106  rnsnopg  5109  resdmres  5122  dmmpt  5126  dmco  5139  co01  5145  fpr  5700  fmptpr  5710  fvsnun2  5716  mpo0  5947  dmoprab  5958  rnoprab  5960  ov6g  6014  1st0  6147  2nd0  6148  dfmpo  6226  algrflem  6232  dftpos2  6264  tposoprab  6283  tposmpo  6284  tfrlem8  6321  frecsuc  6410  df2o3  6433  sbthlemi5  6962  sup00  7004  casedm  7087  djudm  7106  axi2m1  7876  2p2e4  9048  numsuc  9399  numsucc  9425  decmul10add  9454  5p5e10  9456  6p4e10  9457  7p3e10  9460  xnegmnf  9831  pnfaddmnf  9852  fz0tp  10124  fz0to3un2pr  10125  fzo0to2pr  10220  fzo0to3tp  10221  fzo0to42pr  10222  0tonninf  10441  1tonninf  10442  inftonninf  10443  sq4e2t8  10620  i4  10625  fac1  10711  fac3  10714  abs0  11069  absi  11070  trirecip  11511  geoihalfsum  11532  esum  11672  tan0  11741  ef01bndlem  11766  3dvdsdec  11872  3dvds2dec  11873  3lcm2e6woprm  12088  6lcm4e12  12089  ennnfonelem1  12410  ndxarg  12487  setsfun  12499  setsfun0  12500  txbasval  13852  cnmpt1st  13873  cnmpt2nd  13874  dvmptidcn  14263  cos2pi  14310  tan4thpi  14347  sincos6thpi  14348  sqrt2cxp2logb9e3  14478  012of  14830  2o01f  14831  pwf1oexmid  14834  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885