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  3903  dfiunv2  4000  uniop  4341  suc0  4499  unisuc  4501  iunsuc  4508  xpun  4777  dfrn2  4907  dfdmf  4913  dfrnf  4961  res0  5005  resres  5013  xpssres  5036  dfima2  5066  imai  5080  ima0  5083  imaundir  5138  xpima1  5171  xpima2m  5172  dmresv  5183  rescnvcnv  5187  dmtpop  5200  rnsnopg  5203  resdmres  5216  dmmpt  5220  dmco  5233  co01  5239  fpr  5814  fmptpr  5824  fvsnun2  5830  mpo0  6065  dmoprab  6076  rnoprab  6078  ov6g  6134  1st0  6280  2nd0  6281  dfmpo  6359  algrflem  6365  dftpos2  6397  tposoprab  6416  tposmpo  6417  tfrlem8  6454  frecsuc  6543  df2o3  6566  sbthlemi5  7116  sup00  7158  casedm  7241  djudm  7260  axi2m1  8050  2p2e4  9225  numsuc  9579  numsucc  9605  decmul10add  9634  5p5e10  9636  6p4e10  9637  7p3e10  9640  xnegmnf  10013  pnfaddmnf  10034  fz0tp  10306  fz0to3un2pr  10307  fzo0to2pr  10411  fzo0to3tp  10412  fzo0to42pr  10413  0tonninf  10649  1tonninf  10650  inftonninf  10651  sq4e2t8  10846  i4  10851  fac1  10938  fac3  10941  abs0  11555  absi  11556  trirecip  11998  geoihalfsum  12019  esum  12159  tan0  12228  ef01bndlem  12253  3dvds  12361  3dvdsdec  12362  3dvds2dec  12363  3lcm2e6woprm  12594  6lcm4e12  12595  gcdmodi  12930  karatsuba  12939  ennnfonelem1  12964  ndxarg  13041  setsfun  13053  setsfun0  13054  txbasval  14926  cnmpt1st  14947  cnmpt2nd  14948  dvmptidcn  15373  cos2pi  15463  tan4thpi  15500  sincos6thpi  15501  sqrt2cxp2logb9e3  15634  2lgslem3c  15759  2lgslem3d  15760  012of  16288  2o01f  16289  pwf1oexmid  16296  isomninnlem  16329  iswomninnlem  16348  ismkvnnlem  16351