Theorem 3eqtri 2189

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

Syntax hints:   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  csbid  3048  un23  3276  in32  3329  dfrab2  3392  difun2  3483  tpidm23  3671  unisn  3799  dfiunv2  3896  uniop  4227  suc0  4383  unisuc  4385  iunsuc  4392  xpun  4659  dfrn2  4786  dfdmf  4791  dfrnf  4839  res0  4882  resres  4890  xpssres  4913  dfima2  4942  imai  4954  ima0  4957  imaundir  5011  xpima1  5044  xpima2m  5045  dmresv  5056  rescnvcnv  5060  dmtpop  5073  rnsnopg  5076  resdmres  5089  dmmpt  5093  dmco  5106  co01  5112  fpr  5661  fmptpr  5671  fvsnun2  5677  mpo0  5903  dmoprab  5914  rnoprab  5916  ov6g  5970  1st0  6104  2nd0  6105  dfmpo  6182  algrflem  6188  dftpos2  6220  tposoprab  6239  tposmpo  6240  tfrlem8  6277  frecsuc  6366  df2o3  6389  sbthlemi5  6917  sup00  6959  casedm  7042  djudm  7061  axi2m1  7807  2p2e4  8975  numsuc  9326  numsucc  9352  decmul10add  9381  5p5e10  9383  6p4e10  9384  7p3e10  9387  xnegmnf  9756  pnfaddmnf  9777  fz0tp  10047  fz0to3un2pr  10048  fzo0to2pr  10143  fzo0to3tp  10144  fzo0to42pr  10145  0tonninf  10364  1tonninf  10365  inftonninf  10366  sq4e2t8  10542  i4  10547  fac1  10631  fac3  10634  abs0  10986  absi  10987  trirecip  11428  geoihalfsum  11449  esum  11589  tan0  11658  ef01bndlem  11683  3dvdsdec  11787  3dvds2dec  11788  3lcm2e6woprm  11997  6lcm4e12  11998  ennnfonelem1  12277  ndxarg  12354  setsfun  12366  setsfun0  12367  txbasval  12808  cnmpt1st  12829  cnmpt2nd  12830  dvmptidcn  13219  cos2pi  13266  tan4thpi  13303  sincos6thpi  13304  sqrt2cxp2logb9e3  13434  012of  13709  2o01f  13710  pwf1oexmid  13713  isomninnlem  13743  iswomninnlem  13762  ismkvnnlem  13765