Theorem 3eqtr4 1505

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 1498	. 2 |- A = D
5	1, 4	eqtr 1495	1 |- C = D

Syntax hints:   = wceq 956

This theorem is referenced by:  rabswap 1771  rabbii 1805  cbvrab 1910  un23 2189  un4 2190  in23 2225  in4 2226  indir 2253  undir 2254  unrab 2270  inrab 2271  inrab2 2272  difrab 2273  dfnul3 2283  difdifdir 2346  prcom 2447  pwpw0 2469  pwsn 2500  pwsnALT 2501  int0 2547  dfiin2 2588  cbviun 2589  iunun 2613  cbvopab 2672  cbvopab1 2674  cbvopab1s 2675  cbvopab2v 2677  unopab 2679  uniuni 2880  dfom2 3133  xpundi 3225  xpundir 3226  cnvco 3300  dm0 3323  dmsn0 3324  dmsnsn0 3325  dmi 3326  resundi 3378  resundir 3379  rescom 3384  resima 3391  imadmrn 3414  rnun 3457  imaun 3460  rescnvcnv 3493  imacnvcnv 3495  resdmres 3497  imadmres 3498  co01 3509  zfrep6 3614  tfrlem10 3920  tz7.44-2 3929  tz7.44-3 3930  rdglem2 3938  frfnom 3951  dfoprab2 3991  cbvoprab12 3998  cbvoprab3v 4000  resoprab 4009  caopr32 4060  caopr31 4062  caopr4 4064  caoprlem2 4069  fo1st 4091  fo2nd 4092  foprab2 4119  dfec2 4264  snec 4296  map0e 4342  sbthlem6 4452  unfilem1 4548  abfii5OLD 4565  ranksn 4689  rankelun 4707  numthlem 4783  alephcard 4867  xp2cda 4928  dmaddpi 5018  dmmulpi 5019  addasspq 5063  genpdm 5105  prlem936 5155  m1p1sr 5201  m1m1sr 5202  mulgt0sr 5214  axi2m1 5285  mulneg1 5445  divdir 5747  divdiv23 5793  3p3e6 6008  4p3e7 6010  4p4e8 6011  5p3e8 6013  5p4e9 6014  5p5e10 6015  6p3e9 6017  6p4e10 6018  7p3e10 6020  seq1res 6327  seq1shftid 6356  sqdiv 6618  sqreci 6619  binom2 6644  sqr0 6672  sqrlem16 6688  crmul 6740  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 7464  bafval 8223  0vfval 8225  vsfval 8254  cnnvba 8309  cnnvm 8313  ipasslem10 8499  ip2dii 8504  siilem1 8511  efghgrpilem 8719  pilog 8768  h2hcau 8849  h2hlm 8850  hvsubass 8922  hvsub23 8923  hvsubsub4 8926  hvnegdi 8929  his35 8955  normlem3 8978  normlem8 8983  norm-iii 9006  norm3dif 9014  normpar 9021  normpar2 9023  polid2 9024  hhssims 9145  occllem1 9173  projlem3 9188  chjass 9409  chj4 9446  h1de2 9476  spanunsn 9502  fh3 9566  fh4 9567  qlax4 9571  qlaxr3 9577  3oalem5 9611  pjadj 9618  pjsub 9623  pjcj 9629  pjrn 9647  hoadd23 9704  dfbdop2 9786  cnvadj 9816  hhlno 9826  bra0 9874  nmopneg 9889  lnopunilem1 9935  lnophmlem2 9942  branmfnt 10038  cnvtr 10638

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain