Theorem 3eqtr4i 2130

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

Syntax hints:   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  rabswap  2567  rabbiia  2626  cbvrab  2639  cbvcsb  2959  csbco  2964  cbvrabcsf  3015  un4  3183  in13  3236  in31  3237  in4  3239  indifcom  3269  indir  3272  undir  3273  notrab  3300  dfnul3  3313  rab0  3338  prcom  3546  tprot  3563  tpcoma  3564  tpcomb  3565  tpass  3566  qdassr  3568  pw0  3614  opid  3670  int0  3732  cbviun  3797  cbviin  3798  iunrab  3807  iunin1  3824  cbvopab  3939  cbvopab1  3941  cbvopab2  3942  cbvopab1s  3943  cbvopab2v  3945  unopab  3947  cbvmptf  3962  cbvmpt  3963  iunopab  4141  uniuni  4310  2ordpr  4377  rabxp  4514  fconstmpt  4524  inxp  4611  cnvco  4662  rnmpt  4725  resundi  4768  resundir  4769  resindi  4770  resindir  4771  rescom  4780  resima  4788  imadmrn  4827  cnvimarndm  4839  cnvi  4879  rnun  4883  imaundi  4887  cnvxp  4893  imainrect  4920  imacnvcnv  4939  resdmres  4966  imadmres  4967  mptpreima  4968  cbviota  5029  sb8iota  5031  resdif  5323  cbvriota  5672  dfoprab2  5750  cbvoprab1  5775  cbvoprab2  5776  cbvoprab12  5777  cbvoprab3  5779  cbvmpox  5781  resoprab  5799  caov32  5890  caov31  5892  ofmres  5965  dfopab2  6017  dfxp3  6022  dmmpossx  6027  fmpox  6028  tposco  6102  mapsncnv  6519  cbvixp  6539  xpcomco  6649  sbthlemi6  6778  xp2dju  6975  djuassen  6977  dmaddpi  7034  dmmulpi  7035  dfplpq2  7063  dfmpq2  7064  dmaddpq  7088  dmmulpq  7089  axi2m1  7560  negiso  8571  nummac  9078  decsubi  9096  9t11e99  9163  fzprval  9703  fztpval  9704  sqdivapi  10217  binom2i  10242  4bc2eq6  10361  shftidt2  10445  cji  10515  xrnegiso  10870  cbvsum  10968  fsumrelem  11079  nn0gcdsq  11670  restco  12125  cnmptid  12231