Theorem 3eqtr4i 2260

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rabswap  2710  rabbiia  2786  cbvrab  2798  cbvcsbw  3129  cbvcsb  3130  csbco  3135  csbcow  3136  cbvrabcsf  3191  un4  3365  in13  3418  in31  3419  in4  3421  indifcom  3451  indir  3454  undir  3455  notrab  3482  dfnul3  3495  rab0  3521  prcom  3743  tprot  3760  tpcoma  3761  tpcomb  3762  tpass  3763  qdassr  3765  pw0  3816  opid  3876  int0  3938  cbviun  4003  cbviin  4004  iunrab  4014  iunin1  4031  cbvopab  4156  cbvopab1  4158  cbvopab2  4159  cbvopab1s  4160  cbvopab2v  4162  unopab  4164  cbvmptf  4179  cbvmpt  4180  iunopab  4372  uniuni  4544  2ordpr  4618  rabxp  4759  fconstmpt  4769  inxp  4860  cnvco  4911  rnmpt  4976  resundi  5022  resundir  5023  resindi  5024  resindir  5025  rescom  5034  resima  5042  imadmrn  5082  cnvimarndm  5096  cnvi  5137  rnun  5141  imaundi  5145  cnvxp  5151  imainrect  5178  imacnvcnv  5197  resdmres  5224  imadmres  5225  mptpreima  5226  cbviota  5287  cbviotavw  5288  sb8iota  5290  resdif  5600  cbvriotavw  5975  cbvriota  5976  dfoprab2  6061  cbvoprab1  6086  cbvoprab2  6087  cbvoprab12  6088  cbvoprab3  6090  cbvmpox  6092  resoprab  6110  caov32  6203  caov31  6205  ofmres  6291  dfopab2  6345  dfxp3  6352  dmmpossx  6357  fmpox  6358  tposco  6434  mapsncnv  6857  cbvixp  6877  xpcomco  7003  sbthlemi6  7150  xp2dju  7418  djuassen  7420  dmaddpi  7533  dmmulpi  7534  dfplpq2  7562  dfmpq2  7563  dmaddpq  7587  dmmulpq  7588  axi2m1  8083  negiso  9123  nummac  9643  decsubi  9661  9t11e99  9728  fzprval  10305  fztpval  10306  sqdivapi  10873  binom2i  10898  4bc2eq6  11024  shftidt2  11380  cji  11450  xrnegiso  11810  cbvsum  11908  fsumrelem  12019  cbvprod  12106  nn0gcdsq  12759  dec5nprm  12974  dec2nprm  12975  gcdi  12980  decsplit  12989  dfrhm2  14155  rmodislmod  14352  cnfldsub  14576  dvdsrzring  14604  restco  14885  cnmptid  14992  plyid  15457  sincos3rdpi  15554  lgsdir2lem5  15748  lgsquadlem3  15795  2lgslem1b  15805  2lgsoddprmlem3d  15826  vtxval0  15891  iedgval0  15892  if0ab  16311