Theorem 3eqtr4 1508

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr4.1	⊢ A = B
3eqtr4.2	⊢ C = A
3eqtr4.3	⊢ D = B

Assertion

Ref	Expression
3eqtr4	⊢ C = D

Proof of Theorem 3eqtr4

Step	Hyp	Ref	Expression
1		3eqtr4.2	. 2 ⊢ C = A
2		3eqtr4.1	. . 3 ⊢ A = B
3		3eqtr4.3	. . 3 ⊢ D = B
4	2, 3	eqtr4 1501	. 2 ⊢ A = D
5	1, 4	eqtr 1498	1 ⊢ C = D

Syntax hints:   = wceq 958

This theorem is referenced by:  rabswap 1774  rabbii 1808  cbvrab 1913  un23 2192  un4 2193  in23 2228  in4 2229  indir 2256  undir 2257  unrab 2273  inrab 2274  inrab2 2275  difrab 2276  dfnul3 2286  difdifdir 2350  prcom 2451  pwpw0 2473  pwsn 2504  pwsnALT 2505  int0 2551  dfiin2 2592  cbviun 2593  iunun 2618  cbvopab 2677  cbvopab1 2679  cbvopab1s 2680  cbvopab2v 2682  unopab 2684  uniuni 2886  dfom2 3139  xpundi 3231  xpundir 3232  cnvco 3306  dm0 3329  dmsn0 3330  dmsnsn0 3331  dmi 3332  resundi 3384  resundir 3385  rescom 3390  resima 3397  imadmrn 3420  rnun 3463  imaun 3466  rescnvcnv 3499  imacnvcnv 3501  resdmres 3503  imadmres 3504  co01 3515  zfrep6 3620  tfrlem10 3926  tz7.44-2 3935  tz7.44-3 3936  rdglem2 3944  frfnom 3957  dfoprab2 3997  cbvoprab12 4004  cbvoprab3v 4006  resoprab 4015  caopr32 4066  caopr31 4068  caopr4 4070  caoprlem2 4075  fo1st 4097  fo2nd 4098  foprab2 4125  dfec2 4270  snec 4302  map0e 4348  sbthlem6 4458  unfilem1 4560  ranksn 4699  rankelun 4717  numthlem 4793  alephcard 4878  xp2cda 4940  dmaddpi 5030  dmmulpi 5031  addasspq 5075  genpdm 5117  prlem936 5167  m1p1sr 5213  m1m1sr 5214  mulgt0sr 5226  axi2m1 5297  mulneg1 5457  divdir 5754  divdiv23 5795  3p3e6 6010  4p3e7 6012  4p4e8 6013  5p3e8 6015  5p4e9 6016  5p5e10 6017  6p3e9 6019  6p4e10 6020  7p3e10 6022  seq1res 6328  seq1shftid 6357  sqdiv 6619  sqreci 6620  binom2 6645  sqr0 6673  sqrlem16 6689  crmul 6741  cjcj 6778  readd 6784  imadd 6785  cjadd 6788  cjmul 6789  cjmulrcl 6791  reneg 6794  imneg 6796  cjneg 6797  addcj 6798  cji 6827  absmul 6847  absi 6878  faclbnd4lem1 6948  bcpasc2 6967  cbvsum 6986  ser1const 7171  geoser 7234  geolim1i 7238  eirrlem3 7391  eirrlem5 7393  efsep 7396  efcnlem2 7420  sinadd 7451  cosadd 7452  cos2tOLD 7465  bafval 8219  0vfval 8221  vsfval 8250  cnnvba 8305  cnnvm 8309  ipasslem10 8495  ip2dii 8500  siilem1 8507  efghgrpilem 8714  pilog 8763  h2hcau 8844  h2hlm 8845  hvsubass 8917  hvsub23 8918  hvsubsub4 8921  hvnegdi 8924  his35 8950  normlem3 8973  normlem8 8978  norm-iii 9001  norm3dif 9009  normpar 9016  normpar2 9018  polid2 9019  hhssims 9140  occllem1 9168  projlem3 9183  chjass 9404  chj4 9441  h1de2 9471  spanunsn 9497  fh3 9561  fh4 9562  qlax4 9566  qlaxr3 9572  3oalem5 9606  pjadj 9613  pjsub 9618  pjcj 9624  pjrn 9642  hoadd23 9699  dfbdop2 9781  cnvadj 9811  hhlno 9821  bra0 9869  nmopneg 9884  lnopunilem1 9930  lnophmlem2 9937  branmfnt 10033  cnvtr 10609

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472

Copyright terms: Public domain