Theorem 3eqtri 2263

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbid  3155  un23  3388  in32  3443  dfrab2  3508  dfnul4  3522  difun2  3607  if0ab  3641  tpidm23  3812  unisn  3951  dfiunv2  4048  uniop  4398  suc0  4558  unisuc  4560  iunsuc  4567  xpun  4838  dfrn2  4970  dfdmf  4976  dfrnf  5025  res0  5069  resres  5077  xpssres  5100  dfima2  5131  imai  5146  ima0  5149  imaundir  5204  xpima1  5237  xpima2m  5238  dmresv  5249  rescnvcnv  5253  dmtpop  5266  rnsnopg  5269  resdmres  5282  dmmpt  5286  dmco  5299  co01  5305  fpr  5900  fmptpr  5910  fvsnun2  5916  mpo0  6161  dmoprab  6172  rnoprab  6174  ov6g  6230  1st0  6382  2nd0  6383  dfmpo  6463  algrflem  6469  dftpos2  6537  tposoprab  6556  tposmpo  6557  tfrlem8  6594  frecsuc  6683  df2o3  6707  sbthlemi5  7285  sup00  7350  casedm  7433  djudm  7452  axi2m1  8249  2p2e4  9441  numsuc  9801  numsucc  9832  decmul10add  9861  5p5e10  9863  6p4e10  9864  7p3e10  9867  xnegmnf  10248  pnfaddmnf  10269  fz0tp  10546  fz0to3un2pr  10547  fzo0to2pr  10653  fzo0to3tp  10654  fzo0to42pr  10655  0tonninf  10898  1tonninf  10899  inftonninf  10900  sq4e2t8  11095  i4  11100  fac1  11189  fac3  11192  abs0  11846  absi  11847  trirecip  12293  geoihalfsum  12314  esum  12454  tan0  12523  ef01bndlem  12548  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  3lcm2e6woprm  12889  6lcm4e12  12890  gcdmodi  13230  karatsuba  13239  43prm  13265  139prm  13267  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  ballotfilem2  13286  ballotfilemth  13339  ennnfonelem1  13356  ndxarg  13433  setsfun  13445  setsfun0  13446  txbasval  15526  cnmpt1st  15547  cnmpt2nd  15548  dvmptidcn  15973  cos2pi  16064  tan4thpi  16101  sincos6thpi  16102  sqrt2cxp2logb9e3  16244  log2ublem2  16255  log2ublem3  16256  birthdaylog2  16261  cht1  16304  ppi1i  16305  ppi2i  16306  cht2  16309  cht3  16310  bclbnd  16340  bposlem8  16351  2lgslem3c  16452  2lgslem3d  16453  012of  17261  2o01f  17262  pwf1oexmid  17267  isomninnlem  17318  iswomninnlem  17339  ismkvnnlem  17342