Theorem 3eqtr4i 2265

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 2258	. 2 |- D = A
5	1, 4	eqtr4i 2258	1 |- C = D

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  rabswap  2725  rabbiia  2801  cbvrab  2813  cbvcsbw  3144  cbvcsb  3145  csbco  3150  csbcow  3151  cbvrabcsf  3206  un4  3381  in13  3436  in31  3437  in4  3439  indifcom  3469  indir  3472  undir  3473  notrab  3500  dfnul3  3513  rab0  3539  rabsnifsb  3759  prcom  3769  tprot  3786  tpcoma  3787  tpcomb  3788  tpass  3789  qdassr  3791  pw0  3843  opid  3903  int0  3965  cbviun  4030  cbviin  4031  iunrab  4041  iunin1  4058  cbvopab  4183  cbvopab1  4185  cbvopab2  4186  cbvopab1s  4187  cbvopab2v  4189  unopab  4191  cbvmptf  4206  cbvmpt  4207  iunopab  4402  uniuni  4574  2ordpr  4648  rabxp  4789  fconstmpt  4799  inxp  4891  cnvco  4942  rnmpt  5007  resundi  5053  resundir  5054  resindi  5055  resindir  5056  rescom  5065  resima  5073  imadmrn  5113  cnvimarndm  5128  cnvi  5169  rnun  5173  imaundi  5177  cnvxp  5183  imainrect  5210  imacnvcnv  5229  resdmres  5256  imadmres  5257  mptpreima  5258  cbviota  5319  cbviotavw  5320  sb8iota  5322  resdif  5638  cbvriotavw  6016  cbvriota  6017  dfoprab2  6102  cbvoprab1  6127  cbvoprab2  6128  cbvoprab12  6129  cbvoprab3  6131  cbvmpox  6133  resoprab  6151  caov32  6244  caov31  6246  ofmres  6331  dfopab2  6385  dfxp3  6392  dmmpossx  6397  fmpox  6398  tposco  6508  mapsncnv  6932  cbvixp  6952  xpcomco  7079  sbthlemi6  7234  xp2dju  7524  djuassen  7526  dmaddpi  7642  dmmulpi  7643  dfplpq2  7671  dfmpq2  7672  dmaddpq  7696  dmmulpq  7697  axi2m1  8192  negiso  9231  nummac  9756  decsubi  9774  9t11e99  9841  fzprval  10420  fztpval  10421  sqdivapi  10989  binom2i  11014  4bc2eq6  11141  shftidt2  11521  cji  11591  xrnegiso  11951  cbvsum  12049  fsumrelem  12161  cbvprod  12248  nn0gcdsq  12901  dec5nprm  13116  dec2nprm  13117  gcdi  13122  decsplit  13131  dfrhm2  14316  rmodislmod  14516  cnfldsub  14740  dvdsrzring  14768  restco  15056  cnmptid  15163  plyid  15628  sincos3rdpi  15725  lgsdir2lem5  15922  lgsquadlem3  15969  2lgslem1b  15979  2lgsoddprmlem3d  16000  vtxval0  16065  iedgval0  16066