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  6550  mapsncnv  6981  cbvixp  7001  xpcomco  7128  sbthlemi6  7284  xp2dju  7577  djuassen  7579  dmaddpi  7698  dmmulpi  7699  dfplpq2  7727  dfmpq2  7728  dmaddpq  7752  dmmulpq  7753  axi2m1  8248  negiso  9293  nummac  9837  decsubi  9855  9t11e99  9922  fzprval  10506  fztpval  10507  sqdivapi  11081  binom2i  11106  4bc2eq6  11235  shftidt2  11619  cji  11690  xrnegiso  12053  cbvsum  12151  fsumrelem  12263  cbvprod  12350  nn0gcdsq  13005  dec5nprm  13222  dec2nprm  13223  gcdi  13229  decsplit  13238  1259lem1  13271  1259lem4  13274  ballotfilemrinv  13335  gsumcom2fi  14275  dfrhm2  14570  rmodislmod  14797  cnfldsub  15021  dvdsrzring  15047  restco  15400  cnmptid  15507  plyid  15972  sincos3rdpi  16070  log2ublem2  16222  log2ublem3  16223  lgsdir2lem5  16356  lgsquadlem3  16403  2lgslem1b  16413  2lgsoddprmlem3d  16434  vtxval0  16499  iedgval0  16500