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  3443  prcom  3659  tprot  3676  tpcoma  3677  tpcomb  3678  tpass  3679  qdassr  3681  pw0  3727  opid  3783  int0  3845  cbviun  3910  cbviin  3911  iunrab  3920  iunin1  3937  cbvopab  4060  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  cbvopab2v  4066  unopab  4068  cbvmptf  4083  cbvmpt  4084  iunopab  4266  uniuni  4436  2ordpr  4508  rabxp  4648  fconstmpt  4658  inxp  4745  cnvco  4796  rnmpt  4859  resundi  4904  resundir  4905  resindi  4906  resindir  4907  rescom  4916  resima  4924  imadmrn  4963  cnvimarndm  4975  cnvi  5015  rnun  5019  imaundi  5023  cnvxp  5029  imainrect  5056  imacnvcnv  5075  resdmres  5102  imadmres  5103  mptpreima  5104  cbviota  5165  sb8iota  5167  resdif  5464  cbvriota  5819  dfoprab2  5900  cbvoprab1  5925  cbvoprab2  5926  cbvoprab12  5927  cbvoprab3  5929  cbvmpox  5931  resoprab  5949  caov32  6040  caov31  6042  ofmres  6115  dfopab2  6168  dfxp3  6173  dmmpossx  6178  fmpox  6179  tposco  6254  mapsncnv  6673  cbvixp  6693  xpcomco  6804  sbthlemi6  6939  xp2dju  7192  djuassen  7194  dmaddpi  7287  dmmulpi  7288  dfplpq2  7316  dfmpq2  7317  dmaddpq  7341  dmmulpq  7342  axi2m1  7837  negiso  8871  nummac  9387  decsubi  9405  9t11e99  9472  fzprval  10038  fztpval  10039  sqdivapi  10559  binom2i  10584  4bc2eq6  10708  shftidt2  10796  cji  10866  xrnegiso  11225  cbvsum  11323  fsumrelem  11434  cbvprod  11521  nn0gcdsq  12154  restco  12968  cnmptid  13075  sincos3rdpi  13558  lgsdir2lem5  13727  if0ab  13840