Theorem 3eqtr4i 2265

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	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
2		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
3		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
4	2, 3	eqtr4i 2258	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2258	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  rabswap  2725  rabbiia  2801  cbvrab  2813  cbvcsbw  3145  cbvcsb  3146  csbco  3151  csbcow  3152  cbvrabcsf  3207  un4  3383  in13  3438  in31  3439  in4  3441  indifcom  3471  indir  3474  undir  3475  notrab  3502  dfnul3  3515  rab0  3541  rabsnifsb  3762  prcom  3772  tprot  3789  tpcoma  3790  tpcomb  3791  tpass  3792  qdassr  3794  pw0  3846  opid  3906  int0  3968  cbviun  4033  cbviin  4034  iunrab  4044  iunin1  4061  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab2v  4192  unopab  4194  cbvmptf  4209  cbvmpt  4210  iunopab  4405  uniuni  4577  2ordpr  4651  rabxp  4792  fconstmpt  4802  inxp  4894  cnvco  4945  rnmpt  5010  resundi  5056  resundir  5057  resindi  5058  resindir  5059  rescom  5068  resima  5076  imadmrn  5116  cnvimarndm  5131  cnvi  5172  rnun  5176  imaundi  5180  cnvxp  5186  imainrect  5213  imacnvcnv  5232  resdmres  5259  imadmres  5260  mptpreima  5261  cbviota  5322  cbviotavw  5323  sb8iota  5325  resdif  5641  cbvriotavw  6022  cbvriota  6023  dfoprab2  6108  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvoprab3  6137  cbvmpox  6139  resoprab  6157  caov32  6250  caov31  6252  ofmres  6342  dfopab2  6396  dfxp3  6403  dmmpossx  6408  fmpox  6409  tposco  6519  mapsncnv  6943  cbvixp  6963  xpcomco  7090  sbthlemi6  7245  xp2dju  7535  djuassen  7537  dmaddpi  7656  dmmulpi  7657  dfplpq2  7685  dfmpq2  7686  dmaddpq  7710  dmmulpq  7711  axi2m1  8206  negiso  9246  nummac  9771  decsubi  9789  9t11e99  9856  fzprval  10438  fztpval  10439  sqdivapi  11009  binom2i  11034  4bc2eq6  11162  shftidt2  11542  cji  11612  xrnegiso  11972  cbvsum  12070  fsumrelem  12182  cbvprod  12269  nn0gcdsq  12922  dec5nprm  13137  dec2nprm  13138  gcdi  13143  decsplit  13152  ballotfilemrinv  13221  dfrhm2  14399  rmodislmod  14625  cnfldsub  14849  dvdsrzring  14877  restco  15165  cnmptid  15272  plyid  15737  sincos3rdpi  15834  lgsdir2lem5  16031  lgsquadlem3  16078  2lgslem1b  16088  2lgsoddprmlem3d  16109  vtxval0  16174  iedgval0  16175