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  4396  suc0  4556  unisuc  4558  iunsuc  4565  xpun  4836  dfrn2  4968  dfdmf  4974  dfrnf  5023  res0  5067  resres  5075  xpssres  5098  dfima2  5128  imai  5143  ima0  5146  imaundir  5201  xpima1  5234  xpima2m  5235  dmresv  5246  rescnvcnv  5250  dmtpop  5263  rnsnopg  5266  resdmres  5279  dmmpt  5283  dmco  5296  co01  5302  fpr  5897  fmptpr  5907  fvsnun2  5913  mpo0  6158  dmoprab  6169  rnoprab  6171  ov6g  6227  1st0  6378  2nd0  6379  dfmpo  6459  algrflem  6465  dftpos2  6532  tposoprab  6551  tposmpo  6552  tfrlem8  6589  frecsuc  6678  df2o3  6702  sbthlemi5  7278  sup00  7343  casedm  7426  djudm  7445  axi2m1  8242  2p2e4  9432  numsuc  9792  numsucc  9818  decmul10add  9847  5p5e10  9849  6p4e10  9850  7p3e10  9853  xnegmnf  10233  pnfaddmnf  10254  fz0tp  10531  fz0to3un2pr  10532  fzo0to2pr  10638  fzo0to3tp  10639  fzo0to42pr  10640  0tonninf  10879  1tonninf  10880  inftonninf  10881  sq4e2t8  11076  i4  11081  fac1  11169  fac3  11172  abs0  11826  absi  11827  trirecip  12270  geoihalfsum  12291  esum  12431  tan0  12500  ef01bndlem  12525  3dvds  12633  3dvdsdec  12634  3dvds2dec  12635  3lcm2e6woprm  12866  6lcm4e12  12867  gcdmodi  13202  karatsuba  13211  ballotfilem2  13230  ballotfilemth  13283  ennnfonelem1  13300  ndxarg  13377  setsfun  13389  setsfun0  13390  txbasval  15370  cnmpt1st  15391  cnmpt2nd  15392  dvmptidcn  15817  cos2pi  15908  tan4thpi  15945  sincos6thpi  15946  sqrt2cxp2logb9e3  16083  log2ublem2  16090  log2ublem3  16091  birthdaylog2  16096  bclbnd  16127  2lgslem3c  16226  2lgslem3d  16227  012of  17035  2o01f  17036  pwf1oexmid  17041  isomninnlem  17091  iswomninnlem  17111  ismkvnnlem  17114