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 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  csbid  3155  un23  3388  in32  3443  dfrab2  3508  dfnul4  3522  difun2  3607  if0ab  3641  tpidm23  3811  unisn  3949  dfiunv2  4046  uniop  4394  suc0  4554  unisuc  4556  iunsuc  4563  xpun  4834  dfrn2  4966  dfdmf  4972  dfrnf  5021  res0  5065  resres  5073  xpssres  5096  dfima2  5126  imai  5141  ima0  5144  imaundir  5199  xpima1  5232  xpima2m  5233  dmresv  5244  rescnvcnv  5248  dmtpop  5261  rnsnopg  5264  resdmres  5277  dmmpt  5281  dmco  5294  co01  5300  fpr  5891  fmptpr  5901  fvsnun2  5907  mpo0  6152  dmoprab  6163  rnoprab  6165  ov6g  6221  1st0  6372  2nd0  6373  dfmpo  6453  algrflem  6459  dftpos2  6526  tposoprab  6545  tposmpo  6546  tfrlem8  6583  frecsuc  6672  df2o3  6696  sbthlemi5  7272  sup00  7337  casedm  7420  djudm  7439  axi2m1  8236  2p2e4  9414  numsuc  9773  numsucc  9799  decmul10add  9828  5p5e10  9830  6p4e10  9831  7p3e10  9834  xnegmnf  10214  pnfaddmnf  10235  fz0tp  10512  fz0to3un2pr  10513  fzo0to2pr  10619  fzo0to3tp  10620  fzo0to42pr  10621  0tonninf  10860  1tonninf  10861  inftonninf  10862  sq4e2t8  11057  i4  11062  fac1  11150  fac3  11153  abs0  11807  absi  11808  trirecip  12251  geoihalfsum  12272  esum  12412  tan0  12481  ef01bndlem  12506  3dvds  12614  3dvdsdec  12615  3dvds2dec  12616  3lcm2e6woprm  12847  6lcm4e12  12848  gcdmodi  13183  karatsuba  13192  ballotfilem2  13211  ballotfilemth  13264  ennnfonelem1  13281  ndxarg  13358  setsfun  13370  setsfun0  13371  txbasval  15351  cnmpt1st  15372  cnmpt2nd  15373  dvmptidcn  15798  cos2pi  15888  tan4thpi  15925  sincos6thpi  15926  sqrt2cxp2logb9e3  16060  log2ublem2  16067  log2ublem3  16068  birthdaylog2  16073  2lgslem3c  16197  2lgslem3d  16198  012of  17006  2o01f  17007  pwf1oexmid  17012  isomninnlem  17053  iswomninnlem  17073  ismkvnnlem  17076