Theorem 3eqtri 2221

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

Syntax hints:   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  csbid  3092  un23  3323  in32  3376  dfrab2  3439  difun2  3531  tpidm23  3724  unisn  3856  dfiunv2  3953  uniop  4289  suc0  4447  unisuc  4449  iunsuc  4456  xpun  4725  dfrn2  4855  dfdmf  4860  dfrnf  4908  res0  4951  resres  4959  xpssres  4982  dfima2  5012  imai  5026  ima0  5029  imaundir  5084  xpima1  5117  xpima2m  5118  dmresv  5129  rescnvcnv  5133  dmtpop  5146  rnsnopg  5149  resdmres  5162  dmmpt  5166  dmco  5179  co01  5185  fpr  5747  fmptpr  5757  fvsnun2  5763  mpo0  5996  dmoprab  6007  rnoprab  6009  ov6g  6065  1st0  6211  2nd0  6212  dfmpo  6290  algrflem  6296  dftpos2  6328  tposoprab  6347  tposmpo  6348  tfrlem8  6385  frecsuc  6474  df2o3  6497  sbthlemi5  7036  sup00  7078  casedm  7161  djudm  7180  axi2m1  7961  2p2e4  9136  numsuc  9489  numsucc  9515  decmul10add  9544  5p5e10  9546  6p4e10  9547  7p3e10  9550  xnegmnf  9923  pnfaddmnf  9944  fz0tp  10216  fz0to3un2pr  10217  fzo0to2pr  10313  fzo0to3tp  10314  fzo0to42pr  10315  0tonninf  10551  1tonninf  10552  inftonninf  10553  sq4e2t8  10748  i4  10753  fac1  10840  fac3  10843  abs0  11242  absi  11243  trirecip  11685  geoihalfsum  11706  esum  11846  tan0  11915  ef01bndlem  11940  3dvds  12048  3dvdsdec  12049  3dvds2dec  12050  3lcm2e6woprm  12281  6lcm4e12  12282  gcdmodi  12617  karatsuba  12626  ennnfonelem1  12651  ndxarg  12728  setsfun  12740  setsfun0  12741  txbasval  14611  cnmpt1st  14632  cnmpt2nd  14633  dvmptidcn  15058  cos2pi  15148  tan4thpi  15185  sincos6thpi  15186  sqrt2cxp2logb9e3  15319  2lgslem3c  15444  2lgslem3d  15445  012of  15748  2o01f  15749  pwf1oexmid  15754  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809