Theorem 3eqtr4i 2070

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

Syntax hints:   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  rabswap  2488  rabbiia  2547  cbvrab  2555  cbvcsb  2856  csbco  2861  cbvrabcsf  2911  un4  3103  in13  3150  in31  3151  in4  3153  indifcom  3183  indir  3186  undir  3187  notrab  3214  dfnul3  3227  rab0  3246  prcom  3446  tprot  3463  tpcoma  3464  tpcomb  3465  tpass  3466  qdassr  3468  pw0  3511  opid  3567  int0  3629  cbviun  3694  cbviin  3695  iunrab  3704  iunin1  3721  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  unopab  3836  cbvmpt  3851  iunopab  4018  uniuni  4183  2ordpr  4249  rabxp  4380  fconstmpt  4387  inxp  4470  cnvco  4520  rnmpt  4582  resundi  4625  resundir  4626  resindi  4627  resindir  4628  rescom  4636  resima  4643  imadmrn  4678  cnvimarndm  4689  cnvi  4728  rnun  4732  imaundi  4736  cnvxp  4742  imainrect  4766  imacnvcnv  4785  resdmres  4812  imadmres  4813  mptpreima  4814  cbviota  4872  sb8iota  4874  resdif  5148  cbvriota  5478  dfoprab2  5552  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvoprab3  5580  cbvmpt2x  5582  resoprab  5597  caov32  5688  caov31  5690  ofmres  5763  dfopab2  5815  dfxp3  5820  dmmpt2ssx  5825  fmpt2x  5826  tposco  5890  xpcomco  6300  dmaddpi  6423  dmmulpi  6424  dfplpq2  6452  dfmpq2  6453  dmaddpq  6477  dmmulpq  6478  axi2m1  6949  nummac  8399  fzprval  8944  fztpval  8945  sqdivapi  9337  binom2i  9360  shftidt2  9433  cji  9502