Theorem 3eqtr4i 1548

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr4i.1	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4i	|- C = D

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 |- C = A
2		3eqtr4i.1	. . 3 |- A = B
3		3eqtr4i.3	. . 3 |- D = B
4	2, 3	eqtr4i 1541	. 2 |- A = D
5	1, 4	eqtri 1538	1 |- C = D

Syntax hints:   = wceq 992

This theorem is referenced by:  rabswap 1817  rabbii 1851  cbvrab 1956  un23 2241  un4 2242  in23 2277  in4 2278  indir 2305  undir 2306  unrab 2322  inrab 2323  inrab2 2324  difrab 2325  dfnul3 2335  difdifdir 2400  prcom 2508  pwpw0 2533  pwsn 2565  pwsnALT 2566  int0 2614  dfiin2 2656  cbviun 2657  iunun 2683  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  cbvopab2v 2751  unopab 2753  uniuni 3104  dfom2 3220  xpundi 3310  xpundir 3311  cnvco 3391  dm0 3414  dmi 3415  resundi 3465  resundir 3466  resindi 3467  resindir 3468  rescom 3474  resima 3481  imadmrn 3506  rnun 3542  imaundi 3545  rescnvcnv 3591  imacnvcnv 3593  resdmres 3595  imadmres 3596  co01 3613  zfrep6 3721  resdif 3816  dfoprab2 4050  cbvoprab1 4057  cbvoprab12 4058  cbvoprab3v 4060  resoprab 4069  caopr32 4121  caopr31 4123  caopr4 4125  caoprlem2 4130  fo1st 4152  fo2nd 4153  foprab2 4181  fparlem2 4200  tfrlem10 4221  tz7.44-2 4230  tz7.44-3 4231  rdglem2 4239  frfnom 4252  dfec2 4404  snec 4437  map0e 4483  sbthlem6 4597  unfilem1 4694  abfii5 4708  ranksn 4835  rankelun 4853  numthlem 4929  alephcard 5017  xp2cda 5080  dmaddpi 5172  dmmulpi 5173  addasspq 5217  genpdm 5259  prlem936 5309  m1p1sr 5355  m1m1sr 5356  mulgt0sr 5368  axi2m1 5439  mulneg1i 5599  divdiri 5893  divdiv23i 5932  3p3e6 6154  4p3e7 6156  4p4e8 6157  5p3e8 6159  5p4e9 6160  5p5e10 6161  6p3e9 6163  6p4e10 6164  7p3e10 6166  cardfz 6671  seq1res 6692  seq1shftid 6721  sqdivi 6815  sqrecii 6816  binom2i 6841  sqr0 6873  sqrlem16 6889  crmuli 6941  cjcji 6979  readdi 6985  imaddi 6986  cjaddi 6989  cjmuli 6990  cjmulrcli 6992  renegi 6995  imnegi 6997  cjnegi 6998  addcji 6999  cji 7028  absmuli 7049  absi 7081  faclbnd4lem1 7151  bcpasc2i 7170  cbvsumi 7189  ser1consti 7374  geoseri 7439  geolim1i 7443  eirrlem3 7596  eirrlem5 7598  efsepi 7604  efcnlem2 7628  sinaddi 7659  cosaddi 7660  cos2OLD 7673  bafval 8470  0vfval 8472  vsfval 8501  cnnvba 8556  cnnvm 8560  ipasslem10 8755  ip2dii 8760  siilem1 8767  efghgrpilem 8991  pilog 9040  h2hcau 9124  h2hlm 9125  hvsubassi 9197  hvsub23i 9198  hvsubsub4i 9201  hvnegdii 9204  his35i 9231  normlem3 9254  normlem8 9259  norm-iii.i 9282  norm3difi 9290  normpari 9297  normpar2i 9299  polid2i 9300  hhssims 9421  occllem1 9449  projlem3 9464  chjassi 9685  chj4i 9722  h1de2i 9752  spanunsni 9778  fh3i 9842  fh4i 9843  qlax4i 9849  qlaxr3i 9855  3oalem5 9889  pjadjii 9896  pjsubii 9901  pjcji 9907  pjrni 9925  hoadd23i 9984  dfbdop2 10066  cnvadj 10096  hhlnoi 10106  bra0 10154  nmopnegi 10168  lnopunilem1 10214  lnophmlem2 10221  branmfn 10317  branmfnOLD 10318  zrdivrng 10969  subspemp 11060  limfillem2 11102  singempcon 11134  cnvtr 11161  cbviin 11401  cvimarndm 11406  oprabopabf 11807  cbvixpv 11821  piececn 11955  heiborlem42 12052  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain