Theorem 3eqtr4i 2201

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

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  rabswap  2648  rabbiia  2715  cbvrab  2728  cbvcsbw  3053  cbvcsb  3054  csbco  3059  csbcow  3060  cbvrabcsf  3114  un4  3287  in13  3340  in31  3341  in4  3343  indifcom  3373  indir  3376  undir  3377  notrab  3404  dfnul3  3417  rab0  3442  prcom  3657  tprot  3674  tpcoma  3675  tpcomb  3676  tpass  3677  qdassr  3679  pw0  3725  opid  3781  int0  3843  cbviun  3908  cbviin  3909  iunrab  3918  iunin1  3935  cbvopab  4058  cbvopab1  4060  cbvopab2  4061  cbvopab1s  4062  cbvopab2v  4064  unopab  4066  cbvmptf  4081  cbvmpt  4082  iunopab  4264  uniuni  4434  2ordpr  4506  rabxp  4646  fconstmpt  4656  inxp  4743  cnvco  4794  rnmpt  4857  resundi  4902  resundir  4903  resindi  4904  resindir  4905  rescom  4914  resima  4922  imadmrn  4961  cnvimarndm  4973  cnvi  5013  rnun  5017  imaundi  5021  cnvxp  5027  imainrect  5054  imacnvcnv  5073  resdmres  5100  imadmres  5101  mptpreima  5102  cbviota  5163  sb8iota  5165  resdif  5462  cbvriota  5816  dfoprab2  5897  cbvoprab1  5922  cbvoprab2  5923  cbvoprab12  5924  cbvoprab3  5926  cbvmpox  5928  resoprab  5946  caov32  6037  caov31  6039  ofmres  6112  dfopab2  6165  dfxp3  6170  dmmpossx  6175  fmpox  6176  tposco  6251  mapsncnv  6669  cbvixp  6689  xpcomco  6800  sbthlemi6  6935  xp2dju  7179  djuassen  7181  dmaddpi  7274  dmmulpi  7275  dfplpq2  7303  dfmpq2  7304  dmaddpq  7328  dmmulpq  7329  axi2m1  7824  negiso  8858  nummac  9374  decsubi  9392  9t11e99  9459  fzprval  10025  fztpval  10026  sqdivapi  10546  binom2i  10571  4bc2eq6  10695  shftidt2  10783  cji  10853  xrnegiso  11212  cbvsum  11310  fsumrelem  11421  cbvprod  11508  nn0gcdsq  12141  restco  12927  cnmptid  13034  sincos3rdpi  13517  lgsdir2lem5  13686  if0ab  13800