Theorem 3eqtri 2195

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

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  csbid  3057  un23  3286  in32  3339  dfrab2  3402  difun2  3494  tpidm23  3684  unisn  3812  dfiunv2  3909  uniop  4240  suc0  4396  unisuc  4398  iunsuc  4405  xpun  4672  dfrn2  4799  dfdmf  4804  dfrnf  4852  res0  4895  resres  4903  xpssres  4926  dfima2  4955  imai  4967  ima0  4970  imaundir  5024  xpima1  5057  xpima2m  5058  dmresv  5069  rescnvcnv  5073  dmtpop  5086  rnsnopg  5089  resdmres  5102  dmmpt  5106  dmco  5119  co01  5125  fpr  5678  fmptpr  5688  fvsnun2  5694  mpo0  5923  dmoprab  5934  rnoprab  5936  ov6g  5990  1st0  6123  2nd0  6124  dfmpo  6202  algrflem  6208  dftpos2  6240  tposoprab  6259  tposmpo  6260  tfrlem8  6297  frecsuc  6386  df2o3  6409  sbthlemi5  6938  sup00  6980  casedm  7063  djudm  7082  axi2m1  7837  2p2e4  9005  numsuc  9356  numsucc  9382  decmul10add  9411  5p5e10  9413  6p4e10  9414  7p3e10  9417  xnegmnf  9786  pnfaddmnf  9807  fz0tp  10078  fz0to3un2pr  10079  fzo0to2pr  10174  fzo0to3tp  10175  fzo0to42pr  10176  0tonninf  10395  1tonninf  10396  inftonninf  10397  sq4e2t8  10573  i4  10578  fac1  10663  fac3  10666  abs0  11022  absi  11023  trirecip  11464  geoihalfsum  11485  esum  11625  tan0  11694  ef01bndlem  11719  3dvdsdec  11824  3dvds2dec  11825  3lcm2e6woprm  12040  6lcm4e12  12041  ennnfonelem1  12362  ndxarg  12439  setsfun  12451  setsfun0  12452  txbasval  13061  cnmpt1st  13082  cnmpt2nd  13083  dvmptidcn  13472  cos2pi  13519  tan4thpi  13556  sincos6thpi  13557  sqrt2cxp2logb9e3  13687  012of  14028  2o01f  14029  pwf1oexmid  14032  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084