Theorem 3eqtri 2200

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 2196	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2196	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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  csbid  3063  un23  3292  in32  3345  dfrab2  3408  difun2  3500  tpidm23  3690  unisn  3821  dfiunv2  3918  uniop  4249  suc0  4405  unisuc  4407  iunsuc  4414  xpun  4681  dfrn2  4808  dfdmf  4813  dfrnf  4861  res0  4904  resres  4912  xpssres  4935  dfima2  4965  imai  4977  ima0  4980  imaundir  5034  xpima1  5067  xpima2m  5068  dmresv  5079  rescnvcnv  5083  dmtpop  5096  rnsnopg  5099  resdmres  5112  dmmpt  5116  dmco  5129  co01  5135  fpr  5690  fmptpr  5700  fvsnun2  5706  mpo0  5935  dmoprab  5946  rnoprab  5948  ov6g  6002  1st0  6135  2nd0  6136  dfmpo  6214  algrflem  6220  dftpos2  6252  tposoprab  6271  tposmpo  6272  tfrlem8  6309  frecsuc  6398  df2o3  6421  sbthlemi5  6950  sup00  6992  casedm  7075  djudm  7094  axi2m1  7849  2p2e4  9019  numsuc  9370  numsucc  9396  decmul10add  9425  5p5e10  9427  6p4e10  9428  7p3e10  9431  xnegmnf  9800  pnfaddmnf  9821  fz0tp  10092  fz0to3un2pr  10093  fzo0to2pr  10188  fzo0to3tp  10189  fzo0to42pr  10190  0tonninf  10409  1tonninf  10410  inftonninf  10411  sq4e2t8  10587  i4  10592  fac1  10677  fac3  10680  abs0  11035  absi  11036  trirecip  11477  geoihalfsum  11498  esum  11638  tan0  11707  ef01bndlem  11732  3dvdsdec  11837  3dvds2dec  11838  3lcm2e6woprm  12053  6lcm4e12  12054  ennnfonelem1  12375  ndxarg  12452  setsfun  12464  setsfun0  12465  txbasval  13347  cnmpt1st  13368  cnmpt2nd  13369  dvmptidcn  13758  cos2pi  13805  tan4thpi  13842  sincos6thpi  13843  sqrt2cxp2logb9e3  13973  012of  14314  2o01f  14315  pwf1oexmid  14318  isomninnlem  14348  iswomninnlem  14367  ismkvnnlem  14370