Theorem 3eqtr4i 2383

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

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  rabswap  2790  rabbiia  2849  cbvrab  2857  cbvcsb  3140  csbco  3145  cbvrabcsf  3201  un4  3423  in13  3468  in31  3469  in4  3471  indifcom  3500  indir  3503  undir  3504  notrab  3532  symdifcom  3542  dfnul3  3553  rab0  3571  dfif5  3674  prcom  3798  tprot  3815  tpcoma  3816  tpcomb  3817  tpass  3818  qdassr  3820  pwpw0  3855  pwsn  3881  pwsnALT  3882  int0  3940  cbviun  4003  cbviin  4004  iunrab  4013  iunin1  4031  pw0  4160  cbviota  4344  sb8iota  4346  addccom  4406  addc32  4416  nncaddccl  4419  ltfintrilem1  4465  phiun  4614  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  unopab  4638  dfid3  4768  rabxp  4814  xpundi  4832  xpundir  4833  inxp  4863  cnvco  4894  resundi  4981  resundir  4982  resindi  4983  resindir  4984  rescom  4989  resima  5006  imadmrn  5008  cnvimarndm  5017  cnvi  5032  cnvin  5035  rnun  5036  imaundi  5039  cnvxp  5043  resdmres  5078  imadmres  5079  df2nd2  5111  iunfopab  5204  resdif  5306  fvco2  5382  fpr  5437  rnsi  5521  dfoprab2  5558  cbvoprab1  5567  cbvoprab2  5568  cbvoprab12  5569  cbvoprab3  5571  resoprab  5581  caov32  5635  caov31  5637  caov4  5639  caovlem2  5644  cbvmpt  5676  cbvmpt2x  5678  mptpreima  5682  fmpt2x  5730  cnvpprod  5841  rnpprod  5842  dfnnc3  5885  map0e  6023  enmap2lem1  6063  enmap1lem1  6069  muccom  6134  mucass  6135  muc0  6142  ncpw1c  6154  tce2  6236  addccan2nclem2  6264  nchoicelem1  6289  nchoicelem2  6290  nchoicelem16  6304  dmsnfn  6327