Theorem 3eqtri 2263

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	|- A = B
3eqtri.2	|- B = C
3eqtri.3	|- C = D

Assertion

Ref	Expression
3eqtri	|- A = D

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2259	. 2 |- B = D
5	1, 4	eqtri 2259	1 |- A = D

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  7344  casedm  7427  djudm  7446  axi2m1  8243  2p2e4  9434  numsuc  9795  numsucc  9826  decmul10add  9855  5p5e10  9857  6p4e10  9858  7p3e10  9861  xnegmnf  10242  pnfaddmnf  10263  fz0tp  10540  fz0to3un2pr  10541  fzo0to2pr  10647  fzo0to3tp  10648  fzo0to42pr  10649  0tonninf  10892  1tonninf  10893  inftonninf  10894  sq4e2t8  11089  i4  11094  fac1  11183  fac3  11186  abs0  11840  absi  11841  trirecip  12287  geoihalfsum  12308  esum  12448  tan0  12517  ef01bndlem  12542  3dvds  12650  3dvdsdec  12651  3dvds2dec  12652  3lcm2e6woprm  12883  6lcm4e12  12884  gcdmodi  13224  karatsuba  13233  43prm  13259  139prm  13261  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  ballotfilem2  13280  ballotfilemth  13333  ennnfonelem1  13350  ndxarg  13427  setsfun  13439  setsfun0  13440  txbasval  15459  cnmpt1st  15480  cnmpt2nd  15481  dvmptidcn  15906  cos2pi  15997  tan4thpi  16034  sincos6thpi  16035  sqrt2cxp2logb9e3  16172  log2ublem2  16183  log2ublem3  16184  birthdaylog2  16189  cht1  16232  ppi1i  16233  ppi2i  16234  cht2  16237  cht3  16238  bclbnd  16268  bposlem8  16279  2lgslem3c  16380  2lgslem3d  16381  012of  17189  2o01f  17190  pwf1oexmid  17195  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269