Theorem 3eqtr4i 2208

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rabswap  2656  rabbiia  2724  cbvrab  2737  cbvcsbw  3063  cbvcsb  3064  csbco  3069  csbcow  3070  cbvrabcsf  3124  un4  3297  in13  3350  in31  3351  in4  3353  indifcom  3383  indir  3386  undir  3387  notrab  3414  dfnul3  3427  rab0  3453  prcom  3670  tprot  3687  tpcoma  3688  tpcomb  3689  tpass  3690  qdassr  3692  pw0  3741  opid  3798  int0  3860  cbviun  3925  cbviin  3926  iunrab  3936  iunin1  3953  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab2v  4082  unopab  4084  cbvmptf  4099  cbvmpt  4100  iunopab  4283  uniuni  4453  2ordpr  4525  rabxp  4665  fconstmpt  4675  inxp  4763  cnvco  4814  rnmpt  4877  resundi  4922  resundir  4923  resindi  4924  resindir  4925  rescom  4934  resima  4942  imadmrn  4982  cnvimarndm  4994  cnvi  5035  rnun  5039  imaundi  5043  cnvxp  5049  imainrect  5076  imacnvcnv  5095  resdmres  5122  imadmres  5123  mptpreima  5124  cbviota  5185  sb8iota  5187  resdif  5485  cbvriota  5843  dfoprab2  5924  cbvoprab1  5949  cbvoprab2  5950  cbvoprab12  5951  cbvoprab3  5953  cbvmpox  5955  resoprab  5973  caov32  6064  caov31  6066  ofmres  6139  dfopab2  6192  dfxp3  6197  dmmpossx  6202  fmpox  6203  tposco  6278  mapsncnv  6697  cbvixp  6717  xpcomco  6828  sbthlemi6  6963  xp2dju  7216  djuassen  7218  dmaddpi  7326  dmmulpi  7327  dfplpq2  7355  dfmpq2  7356  dmaddpq  7380  dmmulpq  7381  axi2m1  7876  negiso  8914  nummac  9430  decsubi  9448  9t11e99  9515  fzprval  10084  fztpval  10085  sqdivapi  10606  binom2i  10631  4bc2eq6  10756  shftidt2  10843  cji  10913  xrnegiso  11272  cbvsum  11370  fsumrelem  11481  cbvprod  11568  nn0gcdsq  12202  rmodislmod  13446  cnfldsub  13508  dvdsrzring  13532  restco  13713  cnmptid  13820  sincos3rdpi  14303  lgsdir2lem5  14472  2lgsoddprmlem3d  14497  if0ab  14596