Theorem 3eqtr4 1497

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

Syntax hints:   = wceq 953

This theorem is referenced by:  rabswap 1763  rabbii 1796  cbvrab 1901  un23 2179  un4 2180  in23 2215  in4 2216  indir 2243  undir 2244  unrab 2260  inrab 2261  inrab2 2262  difrab 2263  dfnul3 2273  difdifdir 2336  prcom 2437  pwpw0 2460  pwsn 2491  int0 2537  dfiin2 2578  cbviun 2579  iunun 2603  cbvopab 2662  cbvopab1 2664  cbvopab1s 2665  cbvopab2v 2667  unopab 2669  uniuni 2870  dfom2 3123  xpundi 3215  xpundir 3216  cnvco 3289  dm0 3312  dmsn0 3313  dmsnsn0 3314  dmi 3315  resundi 3362  resundir 3363  rescom 3368  resima 3375  imadmrn 3398  rnun 3443  imaun 3446  rescnvcnv 3479  imacnvcnv 3481  resdmres 3483  imadmres 3484  co01 3495  zfrep6 3600  tfrlem10 3905  tz7.44-2 3914  tz7.44-3 3915  rdglem2 3923  frfnom 3936  dfoprab2 3976  cbvoprab12 3983  cbvoprab3v 3985  resoprab 3994  caopr32 4046  caopr31 4048  caopr4 4050  caoprlem2 4055  fo1st 4075  fo2nd 4076  foprab2 4103  dfec2 4248  snec 4280  map0e 4326  sbthlem6 4432  unfilem1 4524  abfii5 4539  ranksn 4661  rankelun 4679  numthlem 4755  alephcard 4839  xp2cda 4900  dmaddpi 4990  dmmulpi 4991  addasspq 5035  genpdm 5077  prlem936 5127  m1p1sr 5173  m1m1sr 5174  mulgt0sr 5186  axi2m1 5257  mulneg1 5417  divdir 5710  divdiv23 5749  3p3e6 5955  4p3e7 5957  4p4e8 5958  5p3e8 5960  5p4e9 5961  5p5e10 5962  6p3e9 5964  6p4e10 5965  7p3e10 5967  seq1res 6264  seq1shftid 6293  sqdiv 6548  sqreci 6549  binom2 6575  sqr0 6602  sqrlem16 6618  crmul 6671  cjcj 6713  readd 6719  imadd 6720  cjadd 6723  cjmul 6724  cjmulrcl 6726  reneg 6729  imneg 6731  cjneg 6732  addcj 6733  cji 6762  absmul 6782  absi 6815  faclbnd4lem1 6885  bcpasc2 6905  cbvsum 6924  ser1const 7107  geoser 7169  geolim1i 7173  eirrlem3 7332  eirrlem5 7334  efsep 7337  efcnlem2 7360  sinadd 7393  cosadd 7394  cos2tOLD 7406  bafval 8161  0vfval 8163  vsfval 8194  cnnvba 8247  cnnvm 8251  ipasslem10 8430  ip2dii 8435  siilem1 8442  efghgrpilem 8634  pilog 8690  h2hcau 8788  h2hlm 8789  hvsubass 8843  hvsub23 8844  hvsubsub4 8847  hvnegdi 8850  his35 8876  normlem3 8899  normlem8 8904  norm-iii 8927  norm3dif 8935  normpar 8942  normpar2 8944  polid2 8945  occllem1 9089  projlem3 9104  chjass 9324  chj4 9361  h1de2 9391  spanunsn 9419  fh3 9483  fh4 9484  qlax4 9488  qlaxr3 9494  3oalem5 9528  pjadj 9535  pjsub 9540  pjcj 9546  pjrn 9564  hoadd23 9621  dfbdop2 9703  cnvadj 9733  hhlno 9743  bra0 9790  nmopneg 9805  lnopunilem1 9850  lnophmlem2 9857  branmfnt 9951  cnvtr 10482

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain