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

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:  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  3773  prcom  3783  tprot  3800  tpcoma  3801  tpcomb  3802  tpass  3803  qdassr  3805  pw0  3857  opid  3917  int0  3979  cbviun  4044  cbviin  4045  iunrab  4055  iunin1  4072  cbvopab  4197  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  cbvopab2v  4203  unopab  4205  cbvmptf  4220  cbvmpt  4221  iunopab  4419  uniuni  4592  2ordpr  4666  rabxp  4807  fconstmpt  4817  inxp  4909  cnvco  4960  rnmpt  5025  resundi  5071  resundir  5072  resindi  5073  resindir  5074  rescom  5083  resima  5091  imadmrn  5131  cnvimarndm  5146  cnvi  5187  rnun  5191  imaundi  5195  cnvxp  5201  imainrect  5228  imacnvcnv  5247  resdmres  5274  imadmres  5275  mptpreima  5276  cbviota  5337  cbviotavw  5338  sb8iota  5340  resdif  5656  cbvriotavw  6039  cbvriota  6040  dfoprab2  6125  cbvoprab1  6150  cbvoprab2  6151  cbvoprab12  6152  cbvoprab3  6154  cbvmpox  6156  resoprab  6174  caov32  6267  caov31  6269  ofmres  6359  dfopab2  6413  dfxp3  6420  dmmpossx  6425  fmpox  6426  tposco  6536  mapsncnv  6967  cbvixp  6987  xpcomco  7114  sbthlemi6  7269  xp2dju  7561  djuassen  7563  dmaddpi  7682  dmmulpi  7683  dfplpq2  7711  dfmpq2  7712  dmaddpq  7736  dmmulpq  7737  axi2m1  8232  negiso  9275  nummac  9800  decsubi  9818  9t11e99  9885  fzprval  10467  fztpval  10468  sqdivapi  11038  binom2i  11063  4bc2eq6  11191  shftidt2  11575  cji  11646  xrnegiso  12006  cbvsum  12104  fsumrelem  12216  cbvprod  12303  nn0gcdsq  12956  dec5nprm  13171  dec2nprm  13172  gcdi  13177  decsplit  13186  ballotfilemrinv  13255  dfrhm2  14434  rmodislmod  14660  cnfldsub  14884  dvdsrzring  14910  restco  15198  cnmptid  15305  plyid  15770  sincos3rdpi  15867  lgsdir2lem5  16065  lgsquadlem3  16112  2lgslem1b  16122  2lgsoddprmlem3d  16143  vtxval0  16208  iedgval0  16209