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  6536  tposoprab  6555  tposmpo  6556  tfrlem8  6593  frecsuc  6682  df2o3  6706  sbthlemi5  7284  sup00  7350  casedm  7433  djudm  7452  axi2m1  8249  2p2e4  9441  numsuc  9802  numsucc  9833  decmul10add  9862  5p5e10  9864  6p4e10  9865  7p3e10  9868  xnegmnf  10249  pnfaddmnf  10270  fz0tp  10547  fz0to3un2pr  10548  fzo0to2pr  10654  fzo0to3tp  10655  fzo0to42pr  10656  0tonninf  10899  1tonninf  10900  inftonninf  10901  sq4e2t8  11096  i4  11101  fac1  11190  fac3  11193  abs0  11847  absi  11848  trirecip  12294  geoihalfsum  12315  esum  12455  tan0  12524  ef01bndlem  12549  3dvds  12657  3dvdsdec  12658  3dvds2dec  12659  3lcm2e6woprm  12890  6lcm4e12  12891  gcdmodi  13231  karatsuba  13240  43prm  13266  139prm  13268  631prm  13271  1259lem1  13272  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  ballotfilem2  13287  ballotfilemth  13340  ennnfonelem1  13357  ndxarg  13434  setsfun  13446  setsfun0  13447  txbasval  15505  cnmpt1st  15526  cnmpt2nd  15527  dvmptidcn  15952  cos2pi  16043  tan4thpi  16080  sincos6thpi  16081  sqrt2cxp2logb9e3  16223  log2ublem2  16234  log2ublem3  16235  birthdaylog2  16240  cht1  16283  ppi1i  16284  ppi2i  16285  cht2  16288  cht3  16289  bclbnd  16319  bposlem8  16330  2lgslem3c  16431  2lgslem3d  16432  012of  17240  2o01f  17241  pwf1oexmid  17246  isomninnlem  17297  iswomninnlem  17318  ismkvnnlem  17321