Theorem 3eqtr4i 2208

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rabswap  2656  rabbiia  2723  cbvrab  2736  cbvcsbw  3062  cbvcsb  3063  csbco  3068  csbcow  3069  cbvrabcsf  3123  un4  3296  in13  3349  in31  3350  in4  3352  indifcom  3382  indir  3385  undir  3386  notrab  3413  dfnul3  3426  rab0  3452  prcom  3669  tprot  3686  tpcoma  3687  tpcomb  3688  tpass  3689  qdassr  3691  pw0  3740  opid  3797  int0  3859  cbviun  3924  cbviin  3925  iunrab  3935  iunin1  3952  cbvopab  4075  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  cbvopab2v  4081  unopab  4083  cbvmptf  4098  cbvmpt  4099  iunopab  4282  uniuni  4452  2ordpr  4524  rabxp  4664  fconstmpt  4674  inxp  4762  cnvco  4813  rnmpt  4876  resundi  4921  resundir  4922  resindi  4923  resindir  4924  rescom  4933  resima  4941  imadmrn  4981  cnvimarndm  4993  cnvi  5034  rnun  5038  imaundi  5042  cnvxp  5048  imainrect  5075  imacnvcnv  5094  resdmres  5121  imadmres  5122  mptpreima  5123  cbviota  5184  sb8iota  5186  resdif  5484  cbvriota  5841  dfoprab2  5922  cbvoprab1  5947  cbvoprab2  5948  cbvoprab12  5949  cbvoprab3  5951  cbvmpox  5953  resoprab  5971  caov32  6062  caov31  6064  ofmres  6137  dfopab2  6190  dfxp3  6195  dmmpossx  6200  fmpox  6201  tposco  6276  mapsncnv  6695  cbvixp  6715  xpcomco  6826  sbthlemi6  6961  xp2dju  7214  djuassen  7216  dmaddpi  7324  dmmulpi  7325  dfplpq2  7353  dfmpq2  7354  dmaddpq  7378  dmmulpq  7379  axi2m1  7874  negiso  8912  nummac  9428  decsubi  9446  9t11e99  9513  fzprval  10082  fztpval  10083  sqdivapi  10604  binom2i  10629  4bc2eq6  10754  shftidt2  10841  cji  10911  xrnegiso  11270  cbvsum  11368  fsumrelem  11479  cbvprod  11566  nn0gcdsq  12200  rmodislmod  13441  cnfldsub  13472  dvdsrzring  13496  restco  13677  cnmptid  13784  sincos3rdpi  14267  lgsdir2lem5  14436  2lgsoddprmlem3d  14461  if0ab  14560