Theorem 3eqtr4i 2238

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 2231	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2231	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  rabswap  2687  rabbiia  2761  cbvrab  2774  cbvcsbw  3105  cbvcsb  3106  csbco  3111  csbcow  3112  cbvrabcsf  3167  un4  3341  in13  3394  in31  3395  in4  3397  indifcom  3427  indir  3430  undir  3431  notrab  3458  dfnul3  3471  rab0  3497  prcom  3719  tprot  3736  tpcoma  3737  tpcomb  3738  tpass  3739  qdassr  3741  pw0  3791  opid  3851  int0  3913  cbviun  3978  cbviin  3979  iunrab  3989  iunin1  4006  cbvopab  4131  cbvopab1  4133  cbvopab2  4134  cbvopab1s  4135  cbvopab2v  4137  unopab  4139  cbvmptf  4154  cbvmpt  4155  iunopab  4346  uniuni  4516  2ordpr  4590  rabxp  4730  fconstmpt  4740  inxp  4830  cnvco  4881  rnmpt  4945  resundi  4991  resundir  4992  resindi  4993  resindir  4994  rescom  5003  resima  5011  imadmrn  5051  cnvimarndm  5065  cnvi  5106  rnun  5110  imaundi  5114  cnvxp  5120  imainrect  5147  imacnvcnv  5166  resdmres  5193  imadmres  5194  mptpreima  5195  cbviota  5256  sb8iota  5258  resdif  5566  cbvriota  5933  dfoprab2  6015  cbvoprab1  6040  cbvoprab2  6041  cbvoprab12  6042  cbvoprab3  6044  cbvmpox  6046  resoprab  6064  caov32  6157  caov31  6159  ofmres  6244  dfopab2  6298  dfxp3  6303  dmmpossx  6308  fmpox  6309  tposco  6384  mapsncnv  6805  cbvixp  6825  xpcomco  6946  sbthlemi6  7090  xp2dju  7358  djuassen  7360  dmaddpi  7473  dmmulpi  7474  dfplpq2  7502  dfmpq2  7503  dmaddpq  7527  dmmulpq  7528  axi2m1  8023  negiso  9063  nummac  9583  decsubi  9601  9t11e99  9668  fzprval  10239  fztpval  10240  sqdivapi  10805  binom2i  10830  4bc2eq6  10956  shftidt2  11258  cji  11328  xrnegiso  11688  cbvsum  11786  fsumrelem  11897  cbvprod  11984  nn0gcdsq  12637  dec5nprm  12852  dec2nprm  12853  gcdi  12858  decsplit  12867  dfrhm2  14031  rmodislmod  14228  cnfldsub  14452  dvdsrzring  14480  restco  14761  cnmptid  14868  plyid  15333  sincos3rdpi  15430  lgsdir2lem5  15624  lgsquadlem3  15671  2lgslem1b  15681  2lgsoddprmlem3d  15702  vtxval0  15765  iedgval0  15766  if0ab  15941