Theorem 3eqtri 2124

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

Syntax hints:   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  csbid  2962  un23  3182  in32  3235  dfrab2  3298  difun2  3389  tpidm23  3571  unisn  3699  dfiunv2  3796  uniop  4115  suc0  4271  unisuc  4273  iunsuc  4280  xpun  4538  dfrn2  4665  dfdmf  4670  dfrnf  4718  res0  4759  resres  4767  xpssres  4790  dfima2  4819  imai  4831  ima0  4834  imaundir  4888  xpima1  4921  xpima2m  4922  dmresv  4933  rescnvcnv  4937  dmtpop  4950  rnsnopg  4953  resdmres  4966  dmmpt  4970  dmco  4983  co01  4989  fpr  5534  fmptpr  5544  fvsnun2  5550  mpo0  5773  dmoprab  5784  rnoprab  5786  ov6g  5840  1st0  5973  2nd0  5974  dfmpo  6050  algrflem  6056  dftpos2  6088  tposoprab  6107  tposmpo  6108  tfrlem8  6145  frecsuc  6234  df2o3  6257  sbthlemi5  6777  sup00  6805  casedm  6886  djudm  6905  axi2m1  7560  2p2e4  8699  numsuc  9047  numsucc  9073  decmul10add  9102  5p5e10  9104  6p4e10  9105  7p3e10  9108  xnegmnf  9453  pnfaddmnf  9474  fz0tp  9742  fzo0to2pr  9836  fzo0to3tp  9837  fzo0to42pr  9838  0tonninf  10053  1tonninf  10054  inftonninf  10055  sq4e2t8  10231  i4  10236  fac1  10316  fac3  10319  abs0  10670  absi  10671  trirecip  11109  geoihalfsum  11130  esum  11166  tan0  11236  ef01bndlem  11261  3dvdsdec  11357  3dvds2dec  11358  3lcm2e6woprm  11560  6lcm4e12  11561  ennnfonelem1  11712  ndxarg  11764  setsfun  11776  setsfun0  11777  txbasval  12217  cnmpt1st  12238  cnmpt2nd  12239  pwf1oexmid  12780  isomninnlem  12809