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  5594  cbvriotavw  5965  cbvriota  5966  dfoprab2  6051  cbvoprab1  6076  cbvoprab2  6077  cbvoprab12  6078  cbvoprab3  6080  cbvmpox  6082  resoprab  6100  caov32  6193  caov31  6195  ofmres  6281  dfopab2  6335  dfxp3  6340  dmmpossx  6345  fmpox  6346  tposco  6421  mapsncnv  6842  cbvixp  6862  xpcomco  6985  sbthlemi6  7129  xp2dju  7397  djuassen  7399  dmaddpi  7512  dmmulpi  7513  dfplpq2  7541  dfmpq2  7542  dmaddpq  7566  dmmulpq  7567  axi2m1  8062  negiso  9102  nummac  9622  decsubi  9640  9t11e99  9707  fzprval  10278  fztpval  10279  sqdivapi  10845  binom2i  10870  4bc2eq6  10996  shftidt2  11343  cji  11413  xrnegiso  11773  cbvsum  11871  fsumrelem  11982  cbvprod  12069  nn0gcdsq  12722  dec5nprm  12937  dec2nprm  12938  gcdi  12943  decsplit  12952  dfrhm2  14118  rmodislmod  14315  cnfldsub  14539  dvdsrzring  14567  restco  14848  cnmptid  14955  plyid  15420  sincos3rdpi  15517  lgsdir2lem5  15711  lgsquadlem3  15758  2lgslem1b  15768  2lgsoddprmlem3d  15789  vtxval0  15854  iedgval0  15855  if0ab  16169