Theorem 3eqtr4i 2227

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rabswap  2676  rabbiia  2748  cbvrab  2761  cbvcsbw  3088  cbvcsb  3089  csbco  3094  csbcow  3095  cbvrabcsf  3150  un4  3323  in13  3376  in31  3377  in4  3379  indifcom  3409  indir  3412  undir  3413  notrab  3440  dfnul3  3453  rab0  3479  prcom  3698  tprot  3715  tpcoma  3716  tpcomb  3717  tpass  3718  qdassr  3720  pw0  3769  opid  3826  int0  3888  cbviun  3953  cbviin  3954  iunrab  3964  iunin1  3981  cbvopab  4104  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  cbvopab2v  4110  unopab  4112  cbvmptf  4127  cbvmpt  4128  iunopab  4316  uniuni  4486  2ordpr  4560  rabxp  4700  fconstmpt  4710  inxp  4800  cnvco  4851  rnmpt  4914  resundi  4959  resundir  4960  resindi  4961  resindir  4962  rescom  4971  resima  4979  imadmrn  5019  cnvimarndm  5033  cnvi  5074  rnun  5078  imaundi  5082  cnvxp  5088  imainrect  5115  imacnvcnv  5134  resdmres  5161  imadmres  5162  mptpreima  5163  cbviota  5224  sb8iota  5226  resdif  5526  cbvriota  5888  dfoprab2  5969  cbvoprab1  5994  cbvoprab2  5995  cbvoprab12  5996  cbvoprab3  5998  cbvmpox  6000  resoprab  6018  caov32  6111  caov31  6113  ofmres  6193  dfopab2  6247  dfxp3  6252  dmmpossx  6257  fmpox  6258  tposco  6333  mapsncnv  6754  cbvixp  6774  xpcomco  6885  sbthlemi6  7028  xp2dju  7282  djuassen  7284  dmaddpi  7392  dmmulpi  7393  dfplpq2  7421  dfmpq2  7422  dmaddpq  7446  dmmulpq  7447  axi2m1  7942  negiso  8982  nummac  9501  decsubi  9519  9t11e99  9586  fzprval  10157  fztpval  10158  sqdivapi  10715  binom2i  10740  4bc2eq6  10866  shftidt2  10997  cji  11067  xrnegiso  11427  cbvsum  11525  fsumrelem  11636  cbvprod  11723  nn0gcdsq  12368  dec5nprm  12583  dec2nprm  12584  gcdi  12589  decsplit  12598  dfrhm2  13710  rmodislmod  13907  cnfldsub  14131  dvdsrzring  14159  restco  14410  cnmptid  14517  plyid  14982  sincos3rdpi  15079  lgsdir2lem5  15273  lgsquadlem3  15320  2lgslem1b  15330  2lgsoddprmlem3d  15351  if0ab  15451