Theorem 3eqtr4i 2224

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	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4i	|- C = D

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 |- C = A
2		3eqtr4i.3	. . 3 |- D = B
3		3eqtr4i.1	. . 3 |- A = B
4	2, 3	eqtr4i 2217	. 2 |- D = A
5	1, 4	eqtr4i 2217	1 |- C = D

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rabswap  2673  rabbiia  2745  cbvrab  2758  cbvcsbw  3084  cbvcsb  3085  csbco  3090  csbcow  3091  cbvrabcsf  3146  un4  3319  in13  3372  in31  3373  in4  3375  indifcom  3405  indir  3408  undir  3409  notrab  3436  dfnul3  3449  rab0  3475  prcom  3694  tprot  3711  tpcoma  3712  tpcomb  3713  tpass  3714  qdassr  3716  pw0  3765  opid  3822  int0  3884  cbviun  3949  cbviin  3950  iunrab  3960  iunin1  3977  cbvopab  4100  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  cbvopab2v  4106  unopab  4108  cbvmptf  4123  cbvmpt  4124  iunopab  4312  uniuni  4482  2ordpr  4556  rabxp  4696  fconstmpt  4706  inxp  4796  cnvco  4847  rnmpt  4910  resundi  4955  resundir  4956  resindi  4957  resindir  4958  rescom  4967  resima  4975  imadmrn  5015  cnvimarndm  5029  cnvi  5070  rnun  5074  imaundi  5078  cnvxp  5084  imainrect  5111  imacnvcnv  5130  resdmres  5157  imadmres  5158  mptpreima  5159  cbviota  5220  sb8iota  5222  resdif  5522  cbvriota  5884  dfoprab2  5965  cbvoprab1  5990  cbvoprab2  5991  cbvoprab12  5992  cbvoprab3  5994  cbvmpox  5996  resoprab  6014  caov32  6106  caov31  6108  ofmres  6188  dfopab2  6242  dfxp3  6247  dmmpossx  6252  fmpox  6253  tposco  6328  mapsncnv  6749  cbvixp  6769  xpcomco  6880  sbthlemi6  7021  xp2dju  7275  djuassen  7277  dmaddpi  7385  dmmulpi  7386  dfplpq2  7414  dfmpq2  7415  dmaddpq  7439  dmmulpq  7440  axi2m1  7935  negiso  8974  nummac  9492  decsubi  9510  9t11e99  9577  fzprval  10148  fztpval  10149  sqdivapi  10694  binom2i  10719  4bc2eq6  10845  shftidt2  10976  cji  11046  xrnegiso  11405  cbvsum  11503  fsumrelem  11614  cbvprod  11701  nn0gcdsq  12338  dfrhm2  13650  rmodislmod  13847  cnfldsub  14063  dvdsrzring  14091  restco  14342  cnmptid  14449  plyid  14892  sincos3rdpi  14978  lgsdir2lem5  15148  2lgsoddprmlem3d  15198  if0ab  15297