Theorem 3eqtri 2221

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 2217	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2217	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbid  3092  un23  3323  in32  3376  dfrab2  3439  difun2  3531  tpidm23  3724  unisn  3856  dfiunv2  3953  uniop  4289  suc0  4447  unisuc  4449  iunsuc  4456  xpun  4725  dfrn2  4855  dfdmf  4860  dfrnf  4908  res0  4951  resres  4959  xpssres  4982  dfima2  5012  imai  5026  ima0  5029  imaundir  5084  xpima1  5117  xpima2m  5118  dmresv  5129  rescnvcnv  5133  dmtpop  5146  rnsnopg  5149  resdmres  5162  dmmpt  5166  dmco  5179  co01  5185  fpr  5747  fmptpr  5757  fvsnun2  5763  mpo0  5996  dmoprab  6007  rnoprab  6009  ov6g  6065  1st0  6211  2nd0  6212  dfmpo  6290  algrflem  6296  dftpos2  6328  tposoprab  6347  tposmpo  6348  tfrlem8  6385  frecsuc  6474  df2o3  6497  sbthlemi5  7036  sup00  7078  casedm  7161  djudm  7180  axi2m1  7959  2p2e4  9134  numsuc  9487  numsucc  9513  decmul10add  9542  5p5e10  9544  6p4e10  9545  7p3e10  9548  xnegmnf  9921  pnfaddmnf  9942  fz0tp  10214  fz0to3un2pr  10215  fzo0to2pr  10311  fzo0to3tp  10312  fzo0to42pr  10313  0tonninf  10549  1tonninf  10550  inftonninf  10551  sq4e2t8  10746  i4  10751  fac1  10838  fac3  10841  abs0  11240  absi  11241  trirecip  11683  geoihalfsum  11704  esum  11844  tan0  11913  ef01bndlem  11938  3dvds  12046  3dvdsdec  12047  3dvds2dec  12048  3lcm2e6woprm  12279  6lcm4e12  12280  gcdmodi  12615  karatsuba  12624  ennnfonelem1  12649  ndxarg  12726  setsfun  12738  setsfun0  12739  txbasval  14587  cnmpt1st  14608  cnmpt2nd  14609  dvmptidcn  15034  cos2pi  15124  tan4thpi  15161  sincos6thpi  15162  sqrt2cxp2logb9e3  15295  2lgslem3c  15420  2lgslem3d  15421  012of  15724  2o01f  15725  pwf1oexmid  15730  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783