Theorem 3eqtr4i 2260

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rabswap  2710  rabbiia  2786  cbvrab  2798  cbvcsbw  3129  cbvcsb  3130  csbco  3135  csbcow  3136  cbvrabcsf  3191  un4  3365  in13  3418  in31  3419  in4  3421  indifcom  3451  indir  3454  undir  3455  notrab  3482  dfnul3  3495  rab0  3521  rabsnifsb  3735  prcom  3745  tprot  3762  tpcoma  3763  tpcomb  3764  tpass  3765  qdassr  3767  pw0  3818  opid  3878  int0  3940  cbviun  4005  cbviin  4006  iunrab  4016  iunin1  4033  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab2v  4164  unopab  4166  cbvmptf  4181  cbvmpt  4182  iunopab  4374  uniuni  4546  2ordpr  4620  rabxp  4761  fconstmpt  4771  inxp  4862  cnvco  4913  rnmpt  4978  resundi  5024  resundir  5025  resindi  5026  resindir  5027  rescom  5036  resima  5044  imadmrn  5084  cnvimarndm  5098  cnvi  5139  rnun  5143  imaundi  5147  cnvxp  5153  imainrect  5180  imacnvcnv  5199  resdmres  5226  imadmres  5227  mptpreima  5228  cbviota  5289  cbviotavw  5290  sb8iota  5292  resdif  5602  cbvriotavw  5977  cbvriota  5978  dfoprab2  6063  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvoprab3  6092  cbvmpox  6094  resoprab  6112  caov32  6205  caov31  6207  ofmres  6293  dfopab2  6347  dfxp3  6354  dmmpossx  6359  fmpox  6360  tposco  6436  mapsncnv  6859  cbvixp  6879  xpcomco  7005  sbthlemi6  7152  xp2dju  7420  djuassen  7422  dmaddpi  7535  dmmulpi  7536  dfplpq2  7564  dfmpq2  7565  dmaddpq  7589  dmmulpq  7590  axi2m1  8085  negiso  9125  nummac  9645  decsubi  9663  9t11e99  9730  fzprval  10307  fztpval  10308  sqdivapi  10875  binom2i  10900  4bc2eq6  11026  shftidt2  11383  cji  11453  xrnegiso  11813  cbvsum  11911  fsumrelem  12022  cbvprod  12109  nn0gcdsq  12762  dec5nprm  12977  dec2nprm  12978  gcdi  12983  decsplit  12992  dfrhm2  14158  rmodislmod  14355  cnfldsub  14579  dvdsrzring  14607  restco  14888  cnmptid  14995  plyid  15460  sincos3rdpi  15557  lgsdir2lem5  15751  lgsquadlem3  15798  2lgslem1b  15808  2lgsoddprmlem3d  15829  vtxval0  15894  iedgval0  15895  if0ab  16337