Theorem 3eqtr4i 2269

Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4i	|- C = D

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 |- C = A
2		3eqtr4i.3	. . 3 |- D = B
3		3eqtr4i.1	. . 3 |- A = B
4	2, 3	eqtr4i 2262	. 2 |- D = A
5	1, 4	eqtr4i 2262	1 |- C = 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:  rabswap  2731  rabbiia  2807  cbvrab  2819  cbvcsbw  3151  cbvcsb  3152  csbco  3157  csbcow  3158  cbvrabcsf  3213  un4  3389  in13  3444  in31  3445  in4  3447  indifcom  3477  indir  3480  undir  3481  notrab  3510  dfnul3  3524  rab0  3551  rabsnifsb  3777  prcom  3787  tprot  3804  tpcoma  3805  tpcomb  3806  tpass  3807  qdassr  3809  pw0  3862  opid  3922  int0  3984  cbviun  4049  cbviin  4050  iunrab  4060  iunin1  4077  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  unopab  4211  cbvmptf  4227  cbvmpt  4228  iunopab  4426  uniuni  4599  2ordpr  4673  rabxp  4814  fconstmpt  4824  inxp  4916  cnvco  4967  rnmpt  5032  resundi  5078  resundir  5079  resindi  5080  resindir  5081  rescom  5090  resima  5098  imadmrn  5139  cnvimarndm  5154  cnvi  5195  rnun  5199  imaundi  5203  cnvxp  5209  imainrect  5236  imacnvcnv  5255  resdmres  5282  imadmres  5283  mptpreima  5284  cbviota  5345  cbviotavw  5346  sb8iota  5348  resdif  5664  cbvriotavw  6052  cbvriota  6053  dfoprab2  6138  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvoprab3  6167  cbvmpox  6169  resoprab  6187  caov32  6280  caov31  6282  ofmres  6373  dfopab2  6427  dfxp3  6434  dmmpossx  6439  fmpox  6440  tposco  6551  mapsncnv  6983  cbvixp  7003  xpcomco  7130  sbthlemi6  7286  xp2dju  7577  djuassen  7579  dmaddpi  7698  dmmulpi  7699  dfplpq2  7727  dfmpq2  7728  dmaddpq  7752  dmmulpq  7753  axi2m1  8248  negiso  9293  nummac  9836  decsubi  9854  9t11e99  9921  fzprval  10505  fztpval  10506  sqdivapi  11080  binom2i  11105  4bc2eq6  11234  shftidt2  11618  cji  11689  xrnegiso  12052  cbvsum  12150  fsumrelem  12262  cbvprod  12349  nn0gcdsq  13004  dec5nprm  13221  dec2nprm  13222  gcdi  13228  decsplit  13237  1259lem1  13270  1259lem4  13273  ballotfilemrinv  13334  gsumcom2fi  14274  dfrhm2  14569  rmodislmod  14796  cnfldsub  15020  dvdsrzring  15046  restco  15417  cnmptid  15524  plyid  15989  sincos3rdpi  16087  log2ublem2  16239  log2ublem3  16240  lgsdir2lem5  16373  lgsquadlem3  16420  2lgslem1b  16430  2lgsoddprmlem3d  16451  vtxval0  16516  iedgval0  16517