Theorem 3eqtri 2259

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  csbid  3149  un23  3382  in32  3437  dfrab2  3500  difun2  3593  if0ab  3627  tpidm23  3797  unisn  3935  dfiunv2  4032  uniop  4377  suc0  4537  unisuc  4539  iunsuc  4546  xpun  4816  dfrn2  4948  dfdmf  4954  dfrnf  5003  res0  5047  resres  5055  xpssres  5078  dfima2  5108  imai  5123  ima0  5126  imaundir  5181  xpima1  5214  xpima2m  5215  dmresv  5226  rescnvcnv  5230  dmtpop  5243  rnsnopg  5246  resdmres  5259  dmmpt  5263  dmco  5276  co01  5282  fpr  5871  fmptpr  5881  fvsnun2  5887  mpo0  6131  dmoprab  6142  rnoprab  6144  ov6g  6200  1st0  6351  2nd0  6352  dfmpo  6432  algrflem  6438  dftpos2  6505  tposoprab  6524  tposmpo  6525  tfrlem8  6562  frecsuc  6651  df2o3  6675  sbthlemi5  7244  sup00  7307  casedm  7390  djudm  7409  axi2m1  8206  2p2e4  9384  numsuc  9743  numsucc  9769  decmul10add  9798  5p5e10  9800  6p4e10  9801  7p3e10  9804  xnegmnf  10184  pnfaddmnf  10205  fz0tp  10481  fz0to3un2pr  10482  fzo0to2pr  10588  fzo0to3tp  10589  fzo0to42pr  10590  0tonninf  10829  1tonninf  10830  inftonninf  10831  sq4e2t8  11026  i4  11031  fac1  11119  fac3  11122  abs0  11772  absi  11773  trirecip  12216  geoihalfsum  12237  esum  12377  tan0  12446  ef01bndlem  12471  3dvds  12579  3dvdsdec  12580  3dvds2dec  12581  3lcm2e6woprm  12812  6lcm4e12  12813  gcdmodi  13148  karatsuba  13157  ballotfilem2  13176  ballotfilemth  13229  ennnfonelem1  13246  ndxarg  13323  setsfun  13335  setsfun0  13336  txbasval  15262  cnmpt1st  15283  cnmpt2nd  15284  dvmptidcn  15709  cos2pi  15799  tan4thpi  15836  sincos6thpi  15837  sqrt2cxp2logb9e3  15970  2lgslem3c  16098  2lgslem3d  16099  012of  16907  2o01f  16908  pwf1oexmid  16913  isomninnlem  16954  iswomninnlem  16974  ismkvnnlem  16977