Theorem 3eqtr4i 2195

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

Syntax hints:   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  rabswap  2642  rabbiia  2706  cbvrab  2719  cbvcsbw  3044  cbvcsb  3045  csbco  3050  csbcow  3051  cbvrabcsf  3105  un4  3277  in13  3330  in31  3331  in4  3333  indifcom  3363  indir  3366  undir  3367  notrab  3394  dfnul3  3407  rab0  3432  prcom  3646  tprot  3663  tpcoma  3664  tpcomb  3665  tpass  3666  qdassr  3668  pw0  3714  opid  3770  int0  3832  cbviun  3897  cbviin  3898  iunrab  3907  iunin1  3924  cbvopab  4047  cbvopab1  4049  cbvopab2  4050  cbvopab1s  4051  cbvopab2v  4053  unopab  4055  cbvmptf  4070  cbvmpt  4071  iunopab  4253  uniuni  4423  2ordpr  4495  rabxp  4635  fconstmpt  4645  inxp  4732  cnvco  4783  rnmpt  4846  resundi  4891  resundir  4892  resindi  4893  resindir  4894  rescom  4903  resima  4911  imadmrn  4950  cnvimarndm  4962  cnvi  5002  rnun  5006  imaundi  5010  cnvxp  5016  imainrect  5043  imacnvcnv  5062  resdmres  5089  imadmres  5090  mptpreima  5091  cbviota  5152  sb8iota  5154  resdif  5448  cbvriota  5802  dfoprab2  5880  cbvoprab1  5905  cbvoprab2  5906  cbvoprab12  5907  cbvoprab3  5909  cbvmpox  5911  resoprab  5929  caov32  6020  caov31  6022  ofmres  6096  dfopab2  6149  dfxp3  6154  dmmpossx  6159  fmpox  6160  tposco  6234  mapsncnv  6652  cbvixp  6672  xpcomco  6783  sbthlemi6  6918  xp2dju  7162  djuassen  7164  dmaddpi  7257  dmmulpi  7258  dfplpq2  7286  dfmpq2  7287  dmaddpq  7311  dmmulpq  7312  axi2m1  7807  negiso  8841  nummac  9357  decsubi  9375  9t11e99  9442  fzprval  10007  fztpval  10008  sqdivapi  10528  binom2i  10553  4bc2eq6  10676  shftidt2  10760  cji  10830  xrnegiso  11189  cbvsum  11287  fsumrelem  11398  cbvprod  11485  nn0gcdsq  12109  restco  12715  cnmptid  12822  sincos3rdpi  13305  if0ab  13522