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	|- 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 2253	. 2 |- D = A
5	1, 4	eqtr4i 2253	1 |- C = D

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  2784  cbvrab  2797  cbvcsbw  3128  cbvcsb  3129  csbco  3134  csbcow  3135  cbvrabcsf  3190  un4  3364  in13  3417  in31  3418  in4  3420  indifcom  3450  indir  3453  undir  3454  notrab  3481  dfnul3  3494  rab0  3520  prcom  3742  tprot  3759  tpcoma  3760  tpcomb  3761  tpass  3762  qdassr  3764  pw0  3815  opid  3875  int0  3937  cbviun  4002  cbviin  4003  iunrab  4013  iunin1  4030  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  unopab  4163  cbvmptf  4178  cbvmpt  4179  iunopab  4370  uniuni  4542  2ordpr  4616  rabxp  4756  fconstmpt  4766  inxp  4856  cnvco  4907  rnmpt  4972  resundi  5018  resundir  5019  resindi  5020  resindir  5021  rescom  5030  resima  5038  imadmrn  5078  cnvimarndm  5092  cnvi  5133  rnun  5137  imaundi  5141  cnvxp  5147  imainrect  5174  imacnvcnv  5193  resdmres  5220  imadmres  5221  mptpreima  5222  cbviota  5283  cbviotavw  5284  sb8iota  5286  resdif  5596  cbvriotavw  5971  cbvriota  5972  dfoprab2  6057  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvoprab3  6086  cbvmpox  6088  resoprab  6106  caov32  6199  caov31  6201  ofmres  6287  dfopab2  6341  dfxp3  6346  dmmpossx  6351  fmpox  6352  tposco  6427  mapsncnv  6850  cbvixp  6870  xpcomco  6993  sbthlemi6  7140  xp2dju  7408  djuassen  7410  dmaddpi  7523  dmmulpi  7524  dfplpq2  7552  dfmpq2  7553  dmaddpq  7577  dmmulpq  7578  axi2m1  8073  negiso  9113  nummac  9633  decsubi  9651  9t11e99  9718  fzprval  10290  fztpval  10291  sqdivapi  10857  binom2i  10882  4bc2eq6  11008  shftidt2  11359  cji  11429  xrnegiso  11789  cbvsum  11887  fsumrelem  11998  cbvprod  12085  nn0gcdsq  12738  dec5nprm  12953  dec2nprm  12954  gcdi  12959  decsplit  12968  dfrhm2  14134  rmodislmod  14331  cnfldsub  14555  dvdsrzring  14583  restco  14864  cnmptid  14971  plyid  15436  sincos3rdpi  15533  lgsdir2lem5  15727  lgsquadlem3  15774  2lgslem1b  15784  2lgsoddprmlem3d  15805  vtxval0  15870  iedgval0  15871  if0ab  16252