Theorem 3eqtri 2218

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

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 2175

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

This theorem is referenced by:  csbid  3088  un23  3318  in32  3371  dfrab2  3434  difun2  3526  tpidm23  3719  unisn  3851  dfiunv2  3948  uniop  4284  suc0  4442  unisuc  4444  iunsuc  4451  xpun  4720  dfrn2  4850  dfdmf  4855  dfrnf  4903  res0  4946  resres  4954  xpssres  4977  dfima2  5007  imai  5021  ima0  5024  imaundir  5079  xpima1  5112  xpima2m  5113  dmresv  5124  rescnvcnv  5128  dmtpop  5141  rnsnopg  5144  resdmres  5157  dmmpt  5161  dmco  5174  co01  5180  fpr  5740  fmptpr  5750  fvsnun2  5756  mpo0  5988  dmoprab  5999  rnoprab  6001  ov6g  6056  1st0  6197  2nd0  6198  dfmpo  6276  algrflem  6282  dftpos2  6314  tposoprab  6333  tposmpo  6334  tfrlem8  6371  frecsuc  6460  df2o3  6483  sbthlemi5  7020  sup00  7062  casedm  7145  djudm  7164  axi2m1  7935  2p2e4  9109  numsuc  9461  numsucc  9487  decmul10add  9516  5p5e10  9518  6p4e10  9519  7p3e10  9522  xnegmnf  9895  pnfaddmnf  9916  fz0tp  10188  fz0to3un2pr  10189  fzo0to2pr  10285  fzo0to3tp  10286  fzo0to42pr  10287  0tonninf  10511  1tonninf  10512  inftonninf  10513  sq4e2t8  10708  i4  10713  fac1  10800  fac3  10803  abs0  11202  absi  11203  trirecip  11644  geoihalfsum  11665  esum  11805  tan0  11874  ef01bndlem  11899  3dvdsdec  12006  3dvds2dec  12007  3lcm2e6woprm  12224  6lcm4e12  12225  ennnfonelem1  12564  ndxarg  12641  setsfun  12653  setsfun0  12654  txbasval  14435  cnmpt1st  14456  cnmpt2nd  14457  dvmptidcn  14863  cos2pi  14939  tan4thpi  14976  sincos6thpi  14977  sqrt2cxp2logb9e3  15107  012of  15486  2o01f  15487  pwf1oexmid  15490  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542