Theorem 3eqtr4i 2208

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rabswap  2655  rabbiia  2722  cbvrab  2735  cbvcsbw  3061  cbvcsb  3062  csbco  3067  csbcow  3068  cbvrabcsf  3122  un4  3295  in13  3348  in31  3349  in4  3351  indifcom  3381  indir  3384  undir  3385  notrab  3412  dfnul3  3425  rab0  3451  prcom  3668  tprot  3685  tpcoma  3686  tpcomb  3687  tpass  3688  qdassr  3690  pw0  3739  opid  3796  int0  3858  cbviun  3923  cbviin  3924  iunrab  3934  iunin1  3951  cbvopab  4074  cbvopab1  4076  cbvopab2  4077  cbvopab1s  4078  cbvopab2v  4080  unopab  4082  cbvmptf  4097  cbvmpt  4098  iunopab  4281  uniuni  4451  2ordpr  4523  rabxp  4663  fconstmpt  4673  inxp  4761  cnvco  4812  rnmpt  4875  resundi  4920  resundir  4921  resindi  4922  resindir  4923  rescom  4932  resima  4940  imadmrn  4980  cnvimarndm  4992  cnvi  5033  rnun  5037  imaundi  5041  cnvxp  5047  imainrect  5074  imacnvcnv  5093  resdmres  5120  imadmres  5121  mptpreima  5122  cbviota  5183  sb8iota  5185  resdif  5483  cbvriota  5840  dfoprab2  5921  cbvoprab1  5946  cbvoprab2  5947  cbvoprab12  5948  cbvoprab3  5950  cbvmpox  5952  resoprab  5970  caov32  6061  caov31  6063  ofmres  6136  dfopab2  6189  dfxp3  6194  dmmpossx  6199  fmpox  6200  tposco  6275  mapsncnv  6694  cbvixp  6714  xpcomco  6825  sbthlemi6  6960  xp2dju  7213  djuassen  7215  dmaddpi  7323  dmmulpi  7324  dfplpq2  7352  dfmpq2  7353  dmaddpq  7377  dmmulpq  7378  axi2m1  7873  negiso  8911  nummac  9427  decsubi  9445  9t11e99  9512  fzprval  10081  fztpval  10082  sqdivapi  10603  binom2i  10628  4bc2eq6  10753  shftidt2  10840  cji  10910  xrnegiso  11269  cbvsum  11367  fsumrelem  11478  cbvprod  11565  nn0gcdsq  12199  cnfldsub  13439  dvdsrzring  13463  restco  13644  cnmptid  13751  sincos3rdpi  14234  lgsdir2lem5  14403  2lgsoddprmlem3d  14428  if0ab  14527