Theorem 3eqtr4i 2236

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 2229	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2229	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  rabswap  2685  rabbiia  2757  cbvrab  2770  cbvcsbw  3097  cbvcsb  3098  csbco  3103  csbcow  3104  cbvrabcsf  3159  un4  3333  in13  3386  in31  3387  in4  3389  indifcom  3419  indir  3422  undir  3423  notrab  3450  dfnul3  3463  rab0  3489  prcom  3709  tprot  3726  tpcoma  3727  tpcomb  3728  tpass  3729  qdassr  3731  pw0  3780  opid  3837  int0  3899  cbviun  3964  cbviin  3965  iunrab  3975  iunin1  3992  cbvopab  4115  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  cbvopab2v  4121  unopab  4123  cbvmptf  4138  cbvmpt  4139  iunopab  4328  uniuni  4498  2ordpr  4572  rabxp  4712  fconstmpt  4722  inxp  4812  cnvco  4863  rnmpt  4926  resundi  4972  resundir  4973  resindi  4974  resindir  4975  rescom  4984  resima  4992  imadmrn  5032  cnvimarndm  5046  cnvi  5087  rnun  5091  imaundi  5095  cnvxp  5101  imainrect  5128  imacnvcnv  5147  resdmres  5174  imadmres  5175  mptpreima  5176  cbviota  5237  sb8iota  5239  resdif  5544  cbvriota  5910  dfoprab2  5992  cbvoprab1  6017  cbvoprab2  6018  cbvoprab12  6019  cbvoprab3  6021  cbvmpox  6023  resoprab  6041  caov32  6134  caov31  6136  ofmres  6221  dfopab2  6275  dfxp3  6280  dmmpossx  6285  fmpox  6286  tposco  6361  mapsncnv  6782  cbvixp  6802  xpcomco  6921  sbthlemi6  7064  xp2dju  7327  djuassen  7329  dmaddpi  7438  dmmulpi  7439  dfplpq2  7467  dfmpq2  7468  dmaddpq  7492  dmmulpq  7493  axi2m1  7988  negiso  9028  nummac  9548  decsubi  9566  9t11e99  9633  fzprval  10204  fztpval  10205  sqdivapi  10768  binom2i  10793  4bc2eq6  10919  shftidt2  11143  cji  11213  xrnegiso  11573  cbvsum  11671  fsumrelem  11782  cbvprod  11869  nn0gcdsq  12522  dec5nprm  12737  dec2nprm  12738  gcdi  12743  decsplit  12752  dfrhm2  13916  rmodislmod  14113  cnfldsub  14337  dvdsrzring  14365  restco  14646  cnmptid  14753  plyid  15218  sincos3rdpi  15315  lgsdir2lem5  15509  lgsquadlem3  15556  2lgslem1b  15566  2lgsoddprmlem3d  15587  vtxval0  15648  iedgval0  15649  if0ab  15741