Theorem 3eqtr4i 2235

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  rabswap  2684  rabbiia  2756  cbvrab  2769  cbvcsbw  3096  cbvcsb  3097  csbco  3102  csbcow  3103  cbvrabcsf  3158  un4  3332  in13  3385  in31  3386  in4  3388  indifcom  3418  indir  3421  undir  3422  notrab  3449  dfnul3  3462  rab0  3488  prcom  3708  tprot  3725  tpcoma  3726  tpcomb  3727  tpass  3728  qdassr  3730  pw0  3779  opid  3836  int0  3898  cbviun  3963  cbviin  3964  iunrab  3974  iunin1  3991  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  cbvopab2v  4120  unopab  4122  cbvmptf  4137  cbvmpt  4138  iunopab  4327  uniuni  4497  2ordpr  4571  rabxp  4711  fconstmpt  4721  inxp  4811  cnvco  4862  rnmpt  4925  resundi  4971  resundir  4972  resindi  4973  resindir  4974  rescom  4983  resima  4991  imadmrn  5031  cnvimarndm  5045  cnvi  5086  rnun  5090  imaundi  5094  cnvxp  5100  imainrect  5127  imacnvcnv  5146  resdmres  5173  imadmres  5174  mptpreima  5175  cbviota  5236  sb8iota  5238  resdif  5543  cbvriota  5909  dfoprab2  5991  cbvoprab1  6016  cbvoprab2  6017  cbvoprab12  6018  cbvoprab3  6020  cbvmpox  6022  resoprab  6040  caov32  6133  caov31  6135  ofmres  6220  dfopab2  6274  dfxp3  6279  dmmpossx  6284  fmpox  6285  tposco  6360  mapsncnv  6781  cbvixp  6801  xpcomco  6920  sbthlemi6  7063  xp2dju  7326  djuassen  7328  dmaddpi  7437  dmmulpi  7438  dfplpq2  7466  dfmpq2  7467  dmaddpq  7491  dmmulpq  7492  axi2m1  7987  negiso  9027  nummac  9547  decsubi  9565  9t11e99  9632  fzprval  10203  fztpval  10204  sqdivapi  10766  binom2i  10791  4bc2eq6  10917  shftidt2  11114  cji  11184  xrnegiso  11544  cbvsum  11642  fsumrelem  11753  cbvprod  11840  nn0gcdsq  12493  dec5nprm  12708  dec2nprm  12709  gcdi  12714  decsplit  12723  dfrhm2  13887  rmodislmod  14084  cnfldsub  14308  dvdsrzring  14336  restco  14617  cnmptid  14724  plyid  15189  sincos3rdpi  15286  lgsdir2lem5  15480  lgsquadlem3  15527  2lgslem1b  15537  2lgsoddprmlem3d  15558  if0ab  15703