Theorem 3eqtr4i 2263

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 2256	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2256	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 2214

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

This theorem is referenced by:  rabswap  2723  rabbiia  2799  cbvrab  2811  cbvcsbw  3142  cbvcsb  3143  csbco  3148  csbcow  3149  cbvrabcsf  3204  un4  3379  in13  3434  in31  3435  in4  3437  indifcom  3467  indir  3470  undir  3471  notrab  3498  dfnul3  3511  rab0  3537  rabsnifsb  3757  prcom  3767  tprot  3784  tpcoma  3785  tpcomb  3786  tpass  3787  qdassr  3789  pw0  3841  opid  3901  int0  3963  cbviun  4028  cbviin  4029  iunrab  4039  iunin1  4056  cbvopab  4181  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  cbvopab2v  4187  unopab  4189  cbvmptf  4204  cbvmpt  4205  iunopab  4400  uniuni  4572  2ordpr  4646  rabxp  4787  fconstmpt  4797  inxp  4889  cnvco  4940  rnmpt  5005  resundi  5051  resundir  5052  resindi  5053  resindir  5054  rescom  5063  resima  5071  imadmrn  5111  cnvimarndm  5126  cnvi  5167  rnun  5171  imaundi  5175  cnvxp  5181  imainrect  5208  imacnvcnv  5227  resdmres  5254  imadmres  5255  mptpreima  5256  cbviota  5317  cbviotavw  5318  sb8iota  5320  resdif  5636  cbvriotavw  6014  cbvriota  6015  dfoprab2  6100  cbvoprab1  6125  cbvoprab2  6126  cbvoprab12  6127  cbvoprab3  6129  cbvmpox  6131  resoprab  6149  caov32  6242  caov31  6244  ofmres  6329  dfopab2  6383  dfxp3  6390  dmmpossx  6395  fmpox  6396  tposco  6506  mapsncnv  6930  cbvixp  6950  xpcomco  7077  sbthlemi6  7232  xp2dju  7522  djuassen  7524  dmaddpi  7640  dmmulpi  7641  dfplpq2  7669  dfmpq2  7670  dmaddpq  7694  dmmulpq  7695  axi2m1  8190  negiso  9229  nummac  9753  decsubi  9771  9t11e99  9838  fzprval  10416  fztpval  10417  sqdivapi  10985  binom2i  11010  4bc2eq6  11137  shftidt2  11517  cji  11587  xrnegiso  11947  cbvsum  12045  fsumrelem  12157  cbvprod  12244  nn0gcdsq  12897  dec5nprm  13112  dec2nprm  13113  gcdi  13118  decsplit  13127  dfrhm2  14299  rmodislmod  14499  cnfldsub  14723  dvdsrzring  14751  restco  15039  cnmptid  15146  plyid  15611  sincos3rdpi  15708  lgsdir2lem5  15905  lgsquadlem3  15952  2lgslem1b  15962  2lgsoddprmlem3d  15983  vtxval0  16048  iedgval0  16049