Theorem 3eqtr4i 2269

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  rabswap  2731  rabbiia  2807  cbvrab  2819  cbvcsbw  3151  cbvcsb  3152  csbco  3157  csbcow  3158  cbvrabcsf  3213  un4  3389  in13  3444  in31  3445  in4  3447  indifcom  3477  indir  3480  undir  3481  notrab  3510  dfnul3  3524  rab0  3551  rabsnifsb  3777  prcom  3787  tprot  3804  tpcoma  3805  tpcomb  3806  tpass  3807  qdassr  3809  pw0  3862  opid  3922  int0  3984  cbviun  4049  cbviin  4050  iunrab  4060  iunin1  4077  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  unopab  4210  cbvmptf  4225  cbvmpt  4226  iunopab  4424  uniuni  4597  2ordpr  4671  rabxp  4812  fconstmpt  4822  inxp  4914  cnvco  4965  rnmpt  5030  resundi  5076  resundir  5077  resindi  5078  resindir  5079  rescom  5088  resima  5096  imadmrn  5136  cnvimarndm  5151  cnvi  5192  rnun  5196  imaundi  5200  cnvxp  5206  imainrect  5233  imacnvcnv  5252  resdmres  5279  imadmres  5280  mptpreima  5281  cbviota  5342  cbviotavw  5343  sb8iota  5345  resdif  5661  cbvriotavw  6049  cbvriota  6050  dfoprab2  6135  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab3  6164  cbvmpox  6166  resoprab  6184  caov32  6277  caov31  6279  ofmres  6369  dfopab2  6423  dfxp3  6430  dmmpossx  6435  fmpox  6436  tposco  6546  mapsncnv  6977  cbvixp  6997  xpcomco  7124  sbthlemi6  7279  xp2dju  7571  djuassen  7573  dmaddpi  7692  dmmulpi  7693  dfplpq2  7721  dfmpq2  7722  dmaddpq  7746  dmmulpq  7747  axi2m1  8242  negiso  9285  nummac  9821  decsubi  9839  9t11e99  9906  fzprval  10489  fztpval  10490  sqdivapi  11060  binom2i  11085  4bc2eq6  11213  shftidt2  11597  cji  11668  xrnegiso  12028  cbvsum  12126  fsumrelem  12238  cbvprod  12325  nn0gcdsq  12978  dec5nprm  13193  dec2nprm  13194  gcdi  13199  decsplit  13208  ballotfilemrinv  13277  dfrhm2  14461  rmodislmod  14688  cnfldsub  14912  dvdsrzring  14938  restco  15275  cnmptid  15382  plyid  15847  sincos3rdpi  15944  log2ublem2  16084  log2ublem3  16085  lgsdir2lem5  16151  lgsquadlem3  16198  2lgslem1b  16208  2lgsoddprmlem3d  16229  vtxval0  16294  iedgval0  16295