Theorem 3eqtri 2162

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

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  csbid  3006  un23  3230  in32  3283  dfrab2  3346  difun2  3437  tpidm23  3619  unisn  3747  dfiunv2  3844  uniop  4172  suc0  4328  unisuc  4330  iunsuc  4337  xpun  4595  dfrn2  4722  dfdmf  4727  dfrnf  4775  res0  4818  resres  4826  xpssres  4849  dfima2  4878  imai  4890  ima0  4893  imaundir  4947  xpima1  4980  xpima2m  4981  dmresv  4992  rescnvcnv  4996  dmtpop  5009  rnsnopg  5012  resdmres  5025  dmmpt  5029  dmco  5042  co01  5048  fpr  5595  fmptpr  5605  fvsnun2  5611  mpo0  5834  dmoprab  5845  rnoprab  5847  ov6g  5901  1st0  6035  2nd0  6036  dfmpo  6113  algrflem  6119  dftpos2  6151  tposoprab  6170  tposmpo  6171  tfrlem8  6208  frecsuc  6297  df2o3  6320  sbthlemi5  6842  sup00  6883  casedm  6964  djudm  6983  axi2m1  7676  2p2e4  8840  numsuc  9188  numsucc  9214  decmul10add  9243  5p5e10  9245  6p4e10  9246  7p3e10  9249  xnegmnf  9605  pnfaddmnf  9626  fz0tp  9894  fzo0to2pr  9988  fzo0to3tp  9989  fzo0to42pr  9990  0tonninf  10205  1tonninf  10206  inftonninf  10207  sq4e2t8  10383  i4  10388  fac1  10468  fac3  10471  abs0  10823  absi  10824  trirecip  11263  geoihalfsum  11284  esum  11357  tan0  11427  ef01bndlem  11452  3dvdsdec  11551  3dvds2dec  11552  3lcm2e6woprm  11756  6lcm4e12  11757  ennnfonelem1  11909  ndxarg  11971  setsfun  11983  setsfun0  11984  txbasval  12425  cnmpt1st  12446  cnmpt2nd  12447  dvmptidcn  12836  cos2pi  12874  tan4thpi  12911  sincos6thpi  12912  pwf1oexmid  13183  isomninnlem  13214