Theorem 3eqtri 2256

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

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

This theorem is referenced by:  csbid  3136  un23  3368  in32  3421  dfrab2  3484  difun2  3576  if0ab  3610  tpidm23  3776  unisn  3914  dfiunv2  4011  uniop  4354  suc0  4514  unisuc  4516  iunsuc  4523  xpun  4793  dfrn2  4924  dfdmf  4930  dfrnf  4979  res0  5023  resres  5031  xpssres  5054  dfima2  5084  imai  5099  ima0  5102  imaundir  5157  xpima1  5190  xpima2m  5191  dmresv  5202  rescnvcnv  5206  dmtpop  5219  rnsnopg  5222  resdmres  5235  dmmpt  5239  dmco  5252  co01  5258  fpr  5844  fmptpr  5854  fvsnun2  5860  mpo0  6101  dmoprab  6112  rnoprab  6114  ov6g  6170  1st0  6316  2nd0  6317  dfmpo  6397  algrflem  6403  dftpos2  6470  tposoprab  6489  tposmpo  6490  tfrlem8  6527  frecsuc  6616  df2o3  6640  sbthlemi5  7203  sup00  7245  casedm  7328  djudm  7347  axi2m1  8138  2p2e4  9313  numsuc  9667  numsucc  9693  decmul10add  9722  5p5e10  9724  6p4e10  9725  7p3e10  9728  xnegmnf  10107  pnfaddmnf  10128  fz0tp  10400  fz0to3un2pr  10401  fzo0to2pr  10507  fzo0to3tp  10508  fzo0to42pr  10509  0tonninf  10746  1tonninf  10747  inftonninf  10748  sq4e2t8  10943  i4  10948  fac1  11035  fac3  11038  abs0  11679  absi  11680  trirecip  12123  geoihalfsum  12144  esum  12284  tan0  12353  ef01bndlem  12378  3dvds  12486  3dvdsdec  12487  3dvds2dec  12488  3lcm2e6woprm  12719  6lcm4e12  12720  gcdmodi  13055  karatsuba  13064  ennnfonelem1  13089  ndxarg  13166  setsfun  13178  setsfun0  13179  txbasval  15058  cnmpt1st  15079  cnmpt2nd  15080  dvmptidcn  15505  cos2pi  15595  tan4thpi  15632  sincos6thpi  15633  sqrt2cxp2logb9e3  15766  2lgslem3c  15894  2lgslem3d  15895  012of  16693  2o01f  16694  pwf1oexmid  16701  isomninnlem  16742  iswomninnlem  16762  ismkvnnlem  16765