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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  rabswap  2712  rabbiia  2788  cbvrab  2800  cbvcsbw  3131  cbvcsb  3132  csbco  3137  csbcow  3138  cbvrabcsf  3193  un4  3367  in13  3420  in31  3421  in4  3423  indifcom  3453  indir  3456  undir  3457  notrab  3484  dfnul3  3497  rab0  3523  rabsnifsb  3737  prcom  3747  tprot  3764  tpcoma  3765  tpcomb  3766  tpass  3767  qdassr  3769  pw0  3820  opid  3880  int0  3942  cbviun  4007  cbviin  4008  iunrab  4018  iunin1  4035  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  unopab  4168  cbvmptf  4183  cbvmpt  4184  iunopab  4376  uniuni  4548  2ordpr  4622  rabxp  4763  fconstmpt  4773  inxp  4864  cnvco  4915  rnmpt  4980  resundi  5026  resundir  5027  resindi  5028  resindir  5029  rescom  5038  resima  5046  imadmrn  5086  cnvimarndm  5100  cnvi  5141  rnun  5145  imaundi  5149  cnvxp  5155  imainrect  5182  imacnvcnv  5201  resdmres  5228  imadmres  5229  mptpreima  5230  cbviota  5291  cbviotavw  5292  sb8iota  5294  resdif  5605  cbvriotavw  5981  cbvriota  5982  dfoprab2  6067  cbvoprab1  6092  cbvoprab2  6093  cbvoprab12  6094  cbvoprab3  6096  cbvmpox  6098  resoprab  6116  caov32  6209  caov31  6211  ofmres  6297  dfopab2  6351  dfxp3  6358  dmmpossx  6363  fmpox  6364  tposco  6440  mapsncnv  6863  cbvixp  6883  xpcomco  7009  sbthlemi6  7160  xp2dju  7429  djuassen  7431  dmaddpi  7544  dmmulpi  7545  dfplpq2  7573  dfmpq2  7574  dmaddpq  7598  dmmulpq  7599  axi2m1  8094  negiso  9134  nummac  9654  decsubi  9672  9t11e99  9739  fzprval  10316  fztpval  10317  sqdivapi  10884  binom2i  10909  4bc2eq6  11035  shftidt2  11392  cji  11462  xrnegiso  11822  cbvsum  11920  fsumrelem  12031  cbvprod  12118  nn0gcdsq  12771  dec5nprm  12986  dec2nprm  12987  gcdi  12992  decsplit  13001  dfrhm2  14167  rmodislmod  14364  cnfldsub  14588  dvdsrzring  14616  restco  14897  cnmptid  15004  plyid  15469  sincos3rdpi  15566  lgsdir2lem5  15760  lgsquadlem3  15807  2lgslem1b  15817  2lgsoddprmlem3d  15838  vtxval0  15903  iedgval0  15904  if0ab  16401