Theorem 3eqtr4i 2236

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  rabswap  2685  rabbiia  2757  cbvrab  2770  cbvcsbw  3097  cbvcsb  3098  csbco  3103  csbcow  3104  cbvrabcsf  3159  un4  3333  in13  3386  in31  3387  in4  3389  indifcom  3419  indir  3422  undir  3423  notrab  3450  dfnul3  3463  rab0  3489  prcom  3709  tprot  3726  tpcoma  3727  tpcomb  3728  tpass  3729  qdassr  3731  pw0  3780  opid  3837  int0  3899  cbviun  3964  cbviin  3965  iunrab  3975  iunin1  3992  cbvopab  4116  cbvopab1  4118  cbvopab2  4119  cbvopab1s  4120  cbvopab2v  4122  unopab  4124  cbvmptf  4139  cbvmpt  4140  iunopab  4329  uniuni  4499  2ordpr  4573  rabxp  4713  fconstmpt  4723  inxp  4813  cnvco  4864  rnmpt  4927  resundi  4973  resundir  4974  resindi  4975  resindir  4976  rescom  4985  resima  4993  imadmrn  5033  cnvimarndm  5047  cnvi  5088  rnun  5092  imaundi  5096  cnvxp  5102  imainrect  5129  imacnvcnv  5148  resdmres  5175  imadmres  5176  mptpreima  5177  cbviota  5238  sb8iota  5240  resdif  5546  cbvriota  5912  dfoprab2  5994  cbvoprab1  6019  cbvoprab2  6020  cbvoprab12  6021  cbvoprab3  6023  cbvmpox  6025  resoprab  6043  caov32  6136  caov31  6138  ofmres  6223  dfopab2  6277  dfxp3  6282  dmmpossx  6287  fmpox  6288  tposco  6363  mapsncnv  6784  cbvixp  6804  xpcomco  6923  sbthlemi6  7066  xp2dju  7329  djuassen  7331  dmaddpi  7440  dmmulpi  7441  dfplpq2  7469  dfmpq2  7470  dmaddpq  7494  dmmulpq  7495  axi2m1  7990  negiso  9030  nummac  9550  decsubi  9568  9t11e99  9635  fzprval  10206  fztpval  10207  sqdivapi  10770  binom2i  10795  4bc2eq6  10921  shftidt2  11176  cji  11246  xrnegiso  11606  cbvsum  11704  fsumrelem  11815  cbvprod  11902  nn0gcdsq  12555  dec5nprm  12770  dec2nprm  12771  gcdi  12776  decsplit  12785  dfrhm2  13949  rmodislmod  14146  cnfldsub  14370  dvdsrzring  14398  restco  14679  cnmptid  14786  plyid  15251  sincos3rdpi  15348  lgsdir2lem5  15542  lgsquadlem3  15589  2lgslem1b  15599  2lgsoddprmlem3d  15620  vtxval0  15681  iedgval0  15682  if0ab  15778