Theorem 3eqtri 2190

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  csbid  3053  un23  3281  in32  3334  dfrab2  3397  difun2  3488  tpidm23  3677  unisn  3805  dfiunv2  3902  uniop  4233  suc0  4389  unisuc  4391  iunsuc  4398  xpun  4665  dfrn2  4792  dfdmf  4797  dfrnf  4845  res0  4888  resres  4896  xpssres  4919  dfima2  4948  imai  4960  ima0  4963  imaundir  5017  xpima1  5050  xpima2m  5051  dmresv  5062  rescnvcnv  5066  dmtpop  5079  rnsnopg  5082  resdmres  5095  dmmpt  5099  dmco  5112  co01  5118  fpr  5667  fmptpr  5677  fvsnun2  5683  mpo0  5912  dmoprab  5923  rnoprab  5925  ov6g  5979  1st0  6112  2nd0  6113  dfmpo  6191  algrflem  6197  dftpos2  6229  tposoprab  6248  tposmpo  6249  tfrlem8  6286  frecsuc  6375  df2o3  6398  sbthlemi5  6926  sup00  6968  casedm  7051  djudm  7070  axi2m1  7816  2p2e4  8984  numsuc  9335  numsucc  9361  decmul10add  9390  5p5e10  9392  6p4e10  9393  7p3e10  9396  xnegmnf  9765  pnfaddmnf  9786  fz0tp  10057  fz0to3un2pr  10058  fzo0to2pr  10153  fzo0to3tp  10154  fzo0to42pr  10155  0tonninf  10374  1tonninf  10375  inftonninf  10376  sq4e2t8  10552  i4  10557  fac1  10642  fac3  10645  abs0  11000  absi  11001  trirecip  11442  geoihalfsum  11463  esum  11603  tan0  11672  ef01bndlem  11697  3dvdsdec  11802  3dvds2dec  11803  3lcm2e6woprm  12018  6lcm4e12  12019  ennnfonelem1  12340  ndxarg  12417  setsfun  12429  setsfun0  12430  txbasval  12907  cnmpt1st  12928  cnmpt2nd  12929  dvmptidcn  13318  cos2pi  13365  tan4thpi  13402  sincos6thpi  13403  sqrt2cxp2logb9e3  13533  012of  13875  2o01f  13876  pwf1oexmid  13879  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931