Theorem 3eqtr4i 2111

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	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
2		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
3		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
4	2, 3	eqtr4i 2104	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2104	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  rabswap  2532  rabbiia  2591  cbvrab  2599  cbvcsb  2912  csbco  2917  cbvrabcsf  2967  un4  3132  in13  3179  in31  3180  in4  3182  indifcom  3210  indir  3213  undir  3214  notrab  3241  dfnul3  3254  rab0  3273  prcom  3468  tprot  3485  tpcoma  3486  tpcomb  3487  tpass  3488  qdassr  3490  pw0  3532  opid  3588  int0  3650  cbviun  3715  cbviin  3716  iunrab  3725  iunin1  3742  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab2v  3855  unopab  3857  cbvmpt  3872  iunopab  4036  uniuni  4201  2ordpr  4267  rabxp  4398  fconstmpt  4405  inxp  4488  cnvco  4538  rnmpt  4600  resundi  4643  resundir  4644  resindi  4645  resindir  4646  rescom  4654  resima  4661  imadmrn  4698  cnvimarndm  4709  cnvi  4748  rnun  4752  imaundi  4756  cnvxp  4762  imainrect  4786  imacnvcnv  4805  resdmres  4832  imadmres  4833  mptpreima  4834  cbviota  4892  sb8iota  4894  resdif  5168  cbvriota  5498  dfoprab2  5572  cbvoprab1  5596  cbvoprab2  5597  cbvoprab12  5598  cbvoprab3  5600  cbvmpt2x  5602  resoprab  5617  caov32  5708  caov31  5710  ofmres  5783  dfopab2  5835  dfxp3  5840  dmmpt2ssx  5845  fmpt2x  5846  tposco  5913  xpcomco  6323  dmaddpi  6515  dmmulpi  6516  dfplpq2  6544  dfmpq2  6545  dmaddpq  6569  dmmulpq  6570  axi2m1  7041  negiso  8033  nummac  8521  decsubi  8539  9t11e99  8606  fzprval  9099  fztpval  9100  sqdivapi  9559  binom2i  9583  4bc2eq6  9701  shftidt2  9720  cji  9789