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  3795  int0  3857  cbviun  3922  cbviin  3923  iunrab  3932  iunin1  3949  cbvopab  4072  cbvopab1  4074  cbvopab2  4075  cbvopab1s  4076  cbvopab2v  4078  unopab  4080  cbvmptf  4095  cbvmpt  4096  iunopab  4279  uniuni  4449  2ordpr  4521  rabxp  4661  fconstmpt  4671  inxp  4758  cnvco  4809  rnmpt  4872  resundi  4917  resundir  4918  resindi  4919  resindir  4920  rescom  4929  resima  4937  imadmrn  4977  cnvimarndm  4989  cnvi  5030  rnun  5034  imaundi  5038  cnvxp  5044  imainrect  5071  imacnvcnv  5090  resdmres  5117  imadmres  5118  mptpreima  5119  cbviota  5180  sb8iota  5182  resdif  5480  cbvriota  5836  dfoprab2  5917  cbvoprab1  5942  cbvoprab2  5943  cbvoprab12  5944  cbvoprab3  5946  cbvmpox  5948  resoprab  5966  caov32  6057  caov31  6059  ofmres  6132  dfopab2  6185  dfxp3  6190  dmmpossx  6195  fmpox  6196  tposco  6271  mapsncnv  6690  cbvixp  6710  xpcomco  6821  sbthlemi6  6956  xp2dju  7209  djuassen  7211  dmaddpi  7319  dmmulpi  7320  dfplpq2  7348  dfmpq2  7349  dmaddpq  7373  dmmulpq  7374  axi2m1  7869  negiso  8906  nummac  9422  decsubi  9440  9t11e99  9507  fzprval  10075  fztpval  10076  sqdivapi  10596  binom2i  10621  4bc2eq6  10745  shftidt2  10832  cji  10902  xrnegiso  11261  cbvsum  11359  fsumrelem  11470  cbvprod  11557  nn0gcdsq  12190  cnfldsub  13274  restco  13456  cnmptid  13563  sincos3rdpi  14046  lgsdir2lem5  14215  if0ab  14328