Theorem 3eqtr4i 2262

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

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

This theorem is referenced by:  rabswap  2713  rabbiia  2789  cbvrab  2801  cbvcsbw  3132  cbvcsb  3133  csbco  3138  csbcow  3139  cbvrabcsf  3194  un4  3369  in13  3422  in31  3423  in4  3425  indifcom  3455  indir  3458  undir  3459  notrab  3486  dfnul3  3499  rab0  3525  rabsnifsb  3741  prcom  3751  tprot  3768  tpcoma  3769  tpcomb  3770  tpass  3771  qdassr  3773  pw0  3825  opid  3885  int0  3947  cbviun  4012  cbviin  4013  iunrab  4023  iunin1  4040  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  unopab  4173  cbvmptf  4188  cbvmpt  4189  iunopab  4382  uniuni  4554  2ordpr  4628  rabxp  4769  fconstmpt  4779  inxp  4870  cnvco  4921  rnmpt  4986  resundi  5032  resundir  5033  resindi  5034  resindir  5035  rescom  5044  resima  5052  imadmrn  5092  cnvimarndm  5107  cnvi  5148  rnun  5152  imaundi  5156  cnvxp  5162  imainrect  5189  imacnvcnv  5208  resdmres  5235  imadmres  5236  mptpreima  5237  cbviota  5298  cbviotavw  5299  sb8iota  5301  resdif  5614  cbvriotavw  5992  cbvriota  5993  dfoprab2  6078  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab3  6107  cbvmpox  6109  resoprab  6127  caov32  6220  caov31  6222  ofmres  6307  dfopab2  6361  dfxp3  6368  dmmpossx  6373  fmpox  6374  tposco  6484  mapsncnv  6907  cbvixp  6927  xpcomco  7053  sbthlemi6  7204  xp2dju  7473  djuassen  7475  dmaddpi  7588  dmmulpi  7589  dfplpq2  7617  dfmpq2  7618  dmaddpq  7642  dmmulpq  7643  axi2m1  8138  negiso  9177  nummac  9699  decsubi  9717  9t11e99  9784  fzprval  10362  fztpval  10363  sqdivapi  10931  binom2i  10956  4bc2eq6  11082  shftidt2  11455  cji  11525  xrnegiso  11885  cbvsum  11983  fsumrelem  12095  cbvprod  12182  nn0gcdsq  12835  dec5nprm  13050  dec2nprm  13051  gcdi  13056  decsplit  13065  dfrhm2  14232  rmodislmod  14430  cnfldsub  14654  dvdsrzring  14682  restco  14968  cnmptid  15075  plyid  15540  sincos3rdpi  15637  lgsdir2lem5  15834  lgsquadlem3  15881  2lgslem1b  15891  2lgsoddprmlem3d  15912  vtxval0  15977  iedgval0  15978