Theorem 3eqtri 2254

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbid  3132  un23  3363  in32  3416  dfrab2  3479  difun2  3571  tpidm23  3767  unisn  3904  dfiunv2  4001  uniop  4343  suc0  4503  unisuc  4505  iunsuc  4512  xpun  4782  dfrn2  4913  dfdmf  4919  dfrnf  4968  res0  5012  resres  5020  xpssres  5043  dfima2  5073  imai  5087  ima0  5090  imaundir  5145  xpima1  5178  xpima2m  5179  dmresv  5190  rescnvcnv  5194  dmtpop  5207  rnsnopg  5210  resdmres  5223  dmmpt  5227  dmco  5240  co01  5246  fpr  5828  fmptpr  5838  fvsnun2  5844  mpo0  6083  dmoprab  6094  rnoprab  6096  ov6g  6152  1st0  6299  2nd0  6300  dfmpo  6380  algrflem  6386  dftpos2  6418  tposoprab  6437  tposmpo  6438  tfrlem8  6475  frecsuc  6564  df2o3  6588  sbthlemi5  7144  sup00  7186  casedm  7269  djudm  7288  axi2m1  8078  2p2e4  9253  numsuc  9607  numsucc  9633  decmul10add  9662  5p5e10  9664  6p4e10  9665  7p3e10  9668  xnegmnf  10042  pnfaddmnf  10063  fz0tp  10335  fz0to3un2pr  10336  fzo0to2pr  10441  fzo0to3tp  10442  fzo0to42pr  10443  0tonninf  10679  1tonninf  10680  inftonninf  10681  sq4e2t8  10876  i4  10881  fac1  10968  fac3  10971  abs0  11590  absi  11591  trirecip  12033  geoihalfsum  12054  esum  12194  tan0  12263  ef01bndlem  12288  3dvds  12396  3dvdsdec  12397  3dvds2dec  12398  3lcm2e6woprm  12629  6lcm4e12  12630  gcdmodi  12965  karatsuba  12974  ennnfonelem1  12999  ndxarg  13076  setsfun  13088  setsfun0  13089  txbasval  14962  cnmpt1st  14983  cnmpt2nd  14984  dvmptidcn  15409  cos2pi  15499  tan4thpi  15536  sincos6thpi  15537  sqrt2cxp2logb9e3  15670  2lgslem3c  15795  2lgslem3d  15796  012of  16470  2o01f  16471  pwf1oexmid  16478  isomninnlem  16512  iswomninnlem  16531  ismkvnnlem  16534