Theorem 3eqtr4i 2262

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

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

This theorem is referenced by:  rabswap  2713  rabbiia  2789  cbvrab  2801  cbvcsbw  3132  cbvcsb  3133  csbco  3138  csbcow  3139  cbvrabcsf  3194  un4  3369  in13  3422  in31  3423  in4  3425  indifcom  3455  indir  3458  undir  3459  notrab  3486  dfnul3  3499  rab0  3525  rabsnifsb  3741  prcom  3751  tprot  3768  tpcoma  3769  tpcomb  3770  tpass  3771  qdassr  3773  pw0  3825  opid  3885  int0  3947  cbviun  4012  cbviin  4013  iunrab  4023  iunin1  4040  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  unopab  4173  cbvmptf  4188  cbvmpt  4189  iunopab  4382  uniuni  4554  2ordpr  4628  rabxp  4769  fconstmpt  4779  inxp  4870  cnvco  4921  rnmpt  4986  resundi  5032  resundir  5033  resindi  5034  resindir  5035  rescom  5044  resima  5052  imadmrn  5092  cnvimarndm  5107  cnvi  5148  rnun  5152  imaundi  5156  cnvxp  5162  imainrect  5189  imacnvcnv  5208  resdmres  5235  imadmres  5236  mptpreima  5237  cbviota  5298  cbviotavw  5299  sb8iota  5301  resdif  5614  cbvriotavw  5992  cbvriota  5993  dfoprab2  6078  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab3  6107  cbvmpox  6109  resoprab  6127  caov32  6220  caov31  6222  ofmres  6307  dfopab2  6361  dfxp3  6368  dmmpossx  6373  fmpox  6374  tposco  6484  mapsncnv  6907  cbvixp  6927  xpcomco  7053  sbthlemi6  7204  xp2dju  7490  djuassen  7492  dmaddpi  7605  dmmulpi  7606  dfplpq2  7634  dfmpq2  7635  dmaddpq  7659  dmmulpq  7660  axi2m1  8155  negiso  9194  nummac  9716  decsubi  9734  9t11e99  9801  fzprval  10379  fztpval  10380  sqdivapi  10948  binom2i  10973  4bc2eq6  11099  shftidt2  11472  cji  11542  xrnegiso  11902  cbvsum  12000  fsumrelem  12112  cbvprod  12199  nn0gcdsq  12852  dec5nprm  13067  dec2nprm  13068  gcdi  13073  decsplit  13082  dfrhm2  14249  rmodislmod  14447  cnfldsub  14671  dvdsrzring  14699  restco  14985  cnmptid  15092  plyid  15557  sincos3rdpi  15654  lgsdir2lem5  15851  lgsquadlem3  15898  2lgslem1b  15908  2lgsoddprmlem3d  15929  vtxval0  15994  iedgval0  15995