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  5982  cbvriota  5983  dfoprab2  6068  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvoprab3  6097  cbvmpox  6099  resoprab  6117  caov32  6210  caov31  6212  ofmres  6298  dfopab2  6352  dfxp3  6359  dmmpossx  6364  fmpox  6365  tposco  6441  mapsncnv  6864  cbvixp  6884  xpcomco  7010  sbthlemi6  7161  xp2dju  7430  djuassen  7432  dmaddpi  7545  dmmulpi  7546  dfplpq2  7574  dfmpq2  7575  dmaddpq  7599  dmmulpq  7600  axi2m1  8095  negiso  9135  nummac  9655  decsubi  9673  9t11e99  9740  fzprval  10317  fztpval  10318  sqdivapi  10886  binom2i  10911  4bc2eq6  11037  shftidt2  11410  cji  11480  xrnegiso  11840  cbvsum  11938  fsumrelem  12050  cbvprod  12137  nn0gcdsq  12790  dec5nprm  13005  dec2nprm  13006  gcdi  13011  decsplit  13020  dfrhm2  14187  rmodislmod  14384  cnfldsub  14608  dvdsrzring  14636  restco  14917  cnmptid  15024  plyid  15489  sincos3rdpi  15586  lgsdir2lem5  15780  lgsquadlem3  15827  2lgslem1b  15837  2lgsoddprmlem3d  15858  vtxval0  15923  iedgval0  15924  if0ab  16452