Theorem 3eqtr4i 2196

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  rabswap  2644  rabbiia  2711  cbvrab  2724  cbvcsbw  3049  cbvcsb  3050  csbco  3055  csbcow  3056  cbvrabcsf  3110  un4  3282  in13  3335  in31  3336  in4  3338  indifcom  3368  indir  3371  undir  3372  notrab  3399  dfnul3  3412  rab0  3437  prcom  3652  tprot  3669  tpcoma  3670  tpcomb  3671  tpass  3672  qdassr  3674  pw0  3720  opid  3776  int0  3838  cbviun  3903  cbviin  3904  iunrab  3913  iunin1  3930  cbvopab  4053  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  cbvopab2v  4059  unopab  4061  cbvmptf  4076  cbvmpt  4077  iunopab  4259  uniuni  4429  2ordpr  4501  rabxp  4641  fconstmpt  4651  inxp  4738  cnvco  4789  rnmpt  4852  resundi  4897  resundir  4898  resindi  4899  resindir  4900  rescom  4909  resima  4917  imadmrn  4956  cnvimarndm  4968  cnvi  5008  rnun  5012  imaundi  5016  cnvxp  5022  imainrect  5049  imacnvcnv  5068  resdmres  5095  imadmres  5096  mptpreima  5097  cbviota  5158  sb8iota  5160  resdif  5454  cbvriota  5808  dfoprab2  5889  cbvoprab1  5914  cbvoprab2  5915  cbvoprab12  5916  cbvoprab3  5918  cbvmpox  5920  resoprab  5938  caov32  6029  caov31  6031  ofmres  6104  dfopab2  6157  dfxp3  6162  dmmpossx  6167  fmpox  6168  tposco  6243  mapsncnv  6661  cbvixp  6681  xpcomco  6792  sbthlemi6  6927  xp2dju  7171  djuassen  7173  dmaddpi  7266  dmmulpi  7267  dfplpq2  7295  dfmpq2  7296  dmaddpq  7320  dmmulpq  7321  axi2m1  7816  negiso  8850  nummac  9366  decsubi  9384  9t11e99  9451  fzprval  10017  fztpval  10018  sqdivapi  10538  binom2i  10563  4bc2eq6  10687  shftidt2  10774  cji  10844  xrnegiso  11203  cbvsum  11301  fsumrelem  11412  cbvprod  11499  nn0gcdsq  12132  restco  12814  cnmptid  12921  sincos3rdpi  13404  lgsdir2lem5  13573  if0ab  13687