Theorem 3eqtr4i 2224

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 2217	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2217	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rabswap  2673  rabbiia  2745  cbvrab  2758  cbvcsbw  3085  cbvcsb  3086  csbco  3091  csbcow  3092  cbvrabcsf  3147  un4  3320  in13  3373  in31  3374  in4  3376  indifcom  3406  indir  3409  undir  3410  notrab  3437  dfnul3  3450  rab0  3476  prcom  3695  tprot  3712  tpcoma  3713  tpcomb  3714  tpass  3715  qdassr  3717  pw0  3766  opid  3823  int0  3885  cbviun  3950  cbviin  3951  iunrab  3961  iunin1  3978  cbvopab  4101  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  cbvopab2v  4107  unopab  4109  cbvmptf  4124  cbvmpt  4125  iunopab  4313  uniuni  4483  2ordpr  4557  rabxp  4697  fconstmpt  4707  inxp  4797  cnvco  4848  rnmpt  4911  resundi  4956  resundir  4957  resindi  4958  resindir  4959  rescom  4968  resima  4976  imadmrn  5016  cnvimarndm  5030  cnvi  5071  rnun  5075  imaundi  5079  cnvxp  5085  imainrect  5112  imacnvcnv  5131  resdmres  5158  imadmres  5159  mptpreima  5160  cbviota  5221  sb8iota  5223  resdif  5523  cbvriota  5885  dfoprab2  5966  cbvoprab1  5991  cbvoprab2  5992  cbvoprab12  5993  cbvoprab3  5995  cbvmpox  5997  resoprab  6015  caov32  6108  caov31  6110  ofmres  6190  dfopab2  6244  dfxp3  6249  dmmpossx  6254  fmpox  6255  tposco  6330  mapsncnv  6751  cbvixp  6771  xpcomco  6882  sbthlemi6  7023  xp2dju  7277  djuassen  7279  dmaddpi  7387  dmmulpi  7388  dfplpq2  7416  dfmpq2  7417  dmaddpq  7441  dmmulpq  7442  axi2m1  7937  negiso  8976  nummac  9495  decsubi  9513  9t11e99  9580  fzprval  10151  fztpval  10152  sqdivapi  10697  binom2i  10722  4bc2eq6  10848  shftidt2  10979  cji  11049  xrnegiso  11408  cbvsum  11506  fsumrelem  11617  cbvprod  11704  nn0gcdsq  12341  dfrhm2  13653  rmodislmod  13850  cnfldsub  14074  dvdsrzring  14102  restco  14353  cnmptid  14460  plyid  14925  sincos3rdpi  15019  lgsdir2lem5  15189  lgsquadlem3  15236  2lgslem1b  15246  2lgsoddprmlem3d  15267  if0ab  15367