Theorem 3eqtr4i 2227

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 2220	. 2 |- D = A
5	1, 4	eqtr4i 2220	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rabswap  2676  rabbiia  2748  cbvrab  2761  cbvcsbw  3088  cbvcsb  3089  csbco  3094  csbcow  3095  cbvrabcsf  3150  un4  3324  in13  3377  in31  3378  in4  3380  indifcom  3410  indir  3413  undir  3414  notrab  3441  dfnul3  3454  rab0  3480  prcom  3699  tprot  3716  tpcoma  3717  tpcomb  3718  tpass  3719  qdassr  3721  pw0  3770  opid  3827  int0  3889  cbviun  3954  cbviin  3955  iunrab  3965  iunin1  3982  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  unopab  4113  cbvmptf  4128  cbvmpt  4129  iunopab  4317  uniuni  4487  2ordpr  4561  rabxp  4701  fconstmpt  4711  inxp  4801  cnvco  4852  rnmpt  4915  resundi  4960  resundir  4961  resindi  4962  resindir  4963  rescom  4972  resima  4980  imadmrn  5020  cnvimarndm  5034  cnvi  5075  rnun  5079  imaundi  5083  cnvxp  5089  imainrect  5116  imacnvcnv  5135  resdmres  5162  imadmres  5163  mptpreima  5164  cbviota  5225  sb8iota  5227  resdif  5529  cbvriota  5891  dfoprab2  5973  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab3  6002  cbvmpox  6004  resoprab  6022  caov32  6115  caov31  6117  ofmres  6202  dfopab2  6256  dfxp3  6261  dmmpossx  6266  fmpox  6267  tposco  6342  mapsncnv  6763  cbvixp  6783  xpcomco  6894  sbthlemi6  7037  xp2dju  7298  djuassen  7300  dmaddpi  7409  dmmulpi  7410  dfplpq2  7438  dfmpq2  7439  dmaddpq  7463  dmmulpq  7464  axi2m1  7959  negiso  8999  nummac  9518  decsubi  9536  9t11e99  9603  fzprval  10174  fztpval  10175  sqdivapi  10732  binom2i  10757  4bc2eq6  10883  shftidt2  11014  cji  11084  xrnegiso  11444  cbvsum  11542  fsumrelem  11653  cbvprod  11740  nn0gcdsq  12393  dec5nprm  12608  dec2nprm  12609  gcdi  12614  decsplit  12623  dfrhm2  13786  rmodislmod  13983  cnfldsub  14207  dvdsrzring  14235  restco  14494  cnmptid  14601  plyid  15066  sincos3rdpi  15163  lgsdir2lem5  15357  lgsquadlem3  15404  2lgslem1b  15414  2lgsoddprmlem3d  15435  if0ab  15535