Theorem 3eqtr4i 2170

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

Syntax hints:   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  rabswap  2609  rabbiia  2671  cbvrab  2684  cbvcsbw  3007  cbvcsb  3008  csbco  3013  cbvrabcsf  3065  un4  3236  in13  3289  in31  3290  in4  3292  indifcom  3322  indir  3325  undir  3326  notrab  3353  dfnul3  3366  rab0  3391  prcom  3599  tprot  3616  tpcoma  3617  tpcomb  3618  tpass  3619  qdassr  3621  pw0  3667  opid  3723  int0  3785  cbviun  3850  cbviin  3851  iunrab  3860  iunin1  3877  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab2v  4005  unopab  4007  cbvmptf  4022  cbvmpt  4023  iunopab  4203  uniuni  4372  2ordpr  4439  rabxp  4576  fconstmpt  4586  inxp  4673  cnvco  4724  rnmpt  4787  resundi  4832  resundir  4833  resindi  4834  resindir  4835  rescom  4844  resima  4852  imadmrn  4891  cnvimarndm  4903  cnvi  4943  rnun  4947  imaundi  4951  cnvxp  4957  imainrect  4984  imacnvcnv  5003  resdmres  5030  imadmres  5031  mptpreima  5032  cbviota  5093  sb8iota  5095  resdif  5389  cbvriota  5740  dfoprab2  5818  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvoprab3  5847  cbvmpox  5849  resoprab  5867  caov32  5958  caov31  5960  ofmres  6034  dfopab2  6087  dfxp3  6092  dmmpossx  6097  fmpox  6098  tposco  6172  mapsncnv  6589  cbvixp  6609  xpcomco  6720  sbthlemi6  6850  xp2dju  7071  djuassen  7073  dmaddpi  7133  dmmulpi  7134  dfplpq2  7162  dfmpq2  7163  dmaddpq  7187  dmmulpq  7188  axi2m1  7683  negiso  8713  nummac  9226  decsubi  9244  9t11e99  9311  fzprval  9862  fztpval  9863  sqdivapi  10376  binom2i  10401  4bc2eq6  10520  shftidt2  10604  cji  10674  xrnegiso  11031  cbvsum  11129  fsumrelem  11240  cbvprod  11327  nn0gcdsq  11878  restco  12343  cnmptid  12450  sincos3rdpi  12924