Theorem 3eqtr4i 2145

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

Syntax hints:   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  rabswap  2583  rabbiia  2642  cbvrab  2655  cbvcsb  2975  csbco  2980  cbvrabcsf  3031  un4  3202  in13  3255  in31  3256  in4  3258  indifcom  3288  indir  3291  undir  3292  notrab  3319  dfnul3  3332  rab0  3357  prcom  3565  tprot  3582  tpcoma  3583  tpcomb  3584  tpass  3585  qdassr  3587  pw0  3633  opid  3689  int0  3751  cbviun  3816  cbviin  3817  iunrab  3826  iunin1  3843  cbvopab  3959  cbvopab1  3961  cbvopab2  3962  cbvopab1s  3963  cbvopab2v  3965  unopab  3967  cbvmptf  3982  cbvmpt  3983  iunopab  4163  uniuni  4332  2ordpr  4399  rabxp  4536  fconstmpt  4546  inxp  4633  cnvco  4684  rnmpt  4747  resundi  4790  resundir  4791  resindi  4792  resindir  4793  rescom  4802  resima  4810  imadmrn  4849  cnvimarndm  4861  cnvi  4901  rnun  4905  imaundi  4909  cnvxp  4915  imainrect  4942  imacnvcnv  4961  resdmres  4988  imadmres  4989  mptpreima  4990  cbviota  5051  sb8iota  5053  resdif  5345  cbvriota  5694  dfoprab2  5772  cbvoprab1  5797  cbvoprab2  5798  cbvoprab12  5799  cbvoprab3  5801  cbvmpox  5803  resoprab  5821  caov32  5912  caov31  5914  ofmres  5988  dfopab2  6041  dfxp3  6046  dmmpossx  6051  fmpox  6052  tposco  6126  mapsncnv  6543  cbvixp  6563  xpcomco  6673  sbthlemi6  6802  xp2dju  7019  djuassen  7021  dmaddpi  7081  dmmulpi  7082  dfplpq2  7110  dfmpq2  7111  dmaddpq  7135  dmmulpq  7136  axi2m1  7610  negiso  8623  nummac  9130  decsubi  9148  9t11e99  9215  fzprval  9755  fztpval  9756  sqdivapi  10269  binom2i  10294  4bc2eq6  10413  shftidt2  10497  cji  10567  xrnegiso  10923  cbvsum  11021  fsumrelem  11132  nn0gcdsq  11723  restco  12186  cnmptid  12292