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  2791  rabbiia  2850  cbvrab  2858  cbvcsb  3141  csbco  3146  cbvrabcsf  3202  un4  3424  in13  3469  in31  3470  in4  3472  indifcom  3501  indir  3504  undir  3505  notrab  3533  symdifcom  3543  dfnul3  3554  rab0  3572  dfif5  3675  prcom  3799  tprot  3816  tpcoma  3817  tpcomb  3818  tpass  3819  qdassr  3821  pwpw0  3856  pwsn  3882  pwsnALT  3883  int0  3941  cbviun  4004  cbviin  4005  iunrab  4014  iunin1  4032  pw0  4161  cbviota  4345  sb8iota  4347  addccom  4407  addc32  4417  nncaddccl  4420  ltfintrilem1  4466  phiun  4615  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab2v  4637  unopab  4639  dfid3  4769  rabxp  4815  xpundi  4833  xpundir  4834  inxp  4864  cnvco  4895  resundi  4982  resundir  4983  resindi  4984  resindir  4985  rescom  4990  resima  5007  imadmrn  5009  cnvimarndm  5018  cnvi  5033  cnvin  5036  rnun  5037  imaundi  5040  cnvxp  5044  resdmres  5079  imadmres  5080  df2nd2  5112  iunfopab  5205  resdif  5307  fvco2  5383  fpr  5438  rnsi  5522  dfoprab2  5559  cbvoprab1  5568  cbvoprab2  5569  cbvoprab12  5570  cbvoprab3  5572  resoprab  5582  caov32  5636  caov31  5638  caov4  5640  caovlem2  5645  cbvmpt  5677  cbvmpt2x  5679  mptpreima  5683  fmpt2x  5731  cnvpprod  5842  rnpprod  5843  dfnnc3  5886  map0e  6024  enmap2lem1  6064  enmap1lem1  6070  muccom  6135  mucass  6136  muc0  6143  ncpw1c  6155  tce2  6237  addccan2nclem2  6265  nchoicelem1  6290  nchoicelem2  6291  nchoicelem16  6305  dmsnfn  6328