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  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  10891  1tonninf  10892  inftonninf  10893  sq4e2t8  11088  i4  11093  fac1  11182  fac3  11185  abs0  11839  absi  11840  trirecip  12286  geoihalfsum  12307  esum  12447  tan0  12516  ef01bndlem  12541  3dvds  12649  3dvdsdec  12650  3dvds2dec  12651  3lcm2e6woprm  12882  6lcm4e12  12883  gcdmodi  13223  karatsuba  13232  43prm  13258  139prm  13260  631prm  13263  1259lem1  13264  1259lem2  13265  1259lem3  13266  1259lem4  13267  1259lem5  13268  ballotfilem2  13279  ballotfilemth  13332  ennnfonelem1  13349  ndxarg  13426  setsfun  13438  setsfun0  13439  txbasval  15420  cnmpt1st  15441  cnmpt2nd  15442  dvmptidcn  15867  cos2pi  15958  tan4thpi  15995  sincos6thpi  15996  sqrt2cxp2logb9e3  16133  log2ublem2  16144  log2ublem3  16145  birthdaylog2  16150  cht1  16193  ppi1i  16194  ppi2i  16195  cht2  16198  cht3  16199  bclbnd  16229  2lgslem3c  16336  2lgslem3d  16337  012of  17145  2o01f  17146  pwf1oexmid  17151  isomninnlem  17201  iswomninnlem  17221  ismkvnnlem  17224