Theorem 3eqtr 1499

Description: An inference from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtr	|- A = D

Proof of Theorem 3eqtr

Step	Hyp	Ref	Expression
1		3eqtr.1	. 2 |- A = B
2		3eqtr.2	. . 3 |- B = C
3		3eqtr.3	. . 3 |- C = D
4	2, 3	eqtr 1495	. 2 |- B = D
5	1, 4	eqtr 1495	1 |- A = D

Syntax hints:   = wceq 956

This theorem is referenced by:  csbid 2005  dfrab2 2274  difin0 2338  undifv 2339  undif1 2340  undif2 2341  difun2 2342  difdifdir 2346  unisn 2517  intsn 2564  unidif0 2739  uniop 2808  dfid3 2836  op1stb 2913  suc0 3043  unisuc 3046  orduniss2 3090  xpun 3227  dfrn2 3303  dfdmf 3306  dfrnf 3348  res0 3371  resres 3377  resopab 3395  dfima2 3405  imai 3417  ima0 3420  rnsnop 3450  imaun2 3461  resdisj 3471  dmresv 3490  rescnvcnv 3493  resdmres 3497  dmco2 3504  fvsnun1 3795  fvsnun2 3796  fopabap 3841  tfrlem8 3918  tz7.44-1 3928  dmoprab 4002  rnoprab 4004  oprabval6g 4032  1st0 4083  2nd0 4084  curry1 4098  df2o2 4141  ecid 4300  qsid 4301  sbthlem5 4451  dfsdom2 4460  mapenlem2 4490  rankpr 4692  rankop 4693  ranksuc 4700  scottexs 4718  scott0s 4719  hta 4728  kmlem3 4767  cda0en 4925  supsrlem2 5226  axmulass 5278  axi2m1 5285  negsub 5381  mulneg1 5445  mulneg2 5446  mul2neg 5447  negsubdi2 5450  ltsubadd 5594  ltneg 5603  divrec 5737  div23 5748  rec11i 5777  prodgt0lem 5818  nnsub 5956  2p2e4 6001  3t3e9 6024  8th4div3 6031  seq11lem 6315  seq0seqz 6542  seq00 6550  cu2 6640  binom2 6644  binom2aOLD 6645  discrlem1 6656  nnesq 6662  sqr0 6672  sqrlem11 6683  sqrlem16 6688  i3 6733  i4 6734  crulem 6736  crmul 6740  crrecz 6741  cjcj 6778  addcj 6798  absi 6878  abslem2i 6908  fac1 6935  fac2 6937  fac3 6938  bcpasc2 6967  binomlem6 7071  iserzshft 7144  fnsmnt 7226  geolim1i 7238  0.999... 7246  eval 7309  erelem6 7324  ege2lem2 7328  ege2le3lem2 7329  efcj 7336  efaddlem6 7343  efaddlem16 7353  eirrlem1 7389  eft0val 7398  ef4p 7399  efge1p 7402  sin0 7444  cos0 7446  sinadd 7451  cosadd 7452  sin01bndlem1 7467  acdc2lem2 7489  acdc5lem2 7492  ruclem6 7515  ruclem12 7521  ruclem15 7524  infmap2lem1 7579  subtop 7646  indistps 7653  remetba 7909  vsfval 8254  nvpi 8294  ipval2 8357  ip0i 8484  ip1ilem 8485  ip2i 8487  ipdirilem 8488  ipasslem10 8499  spwval2 8653  pilem3 8673  eulerid 8683  sin2pi 8684  cos2pi 8685  sincosq4sgn 8707  sincos6thpi 8711  dfrelog 8756  pilog 8768  hvnegdi 8929  hvsubeq0 8930  hvsubcan2 8931  hvaddcan 8932  hvsubadd 8933  hisubcom 8970  normlem0 8975  normlem1 8976  normlem3 8978  normlem9 8984  bcseq 8986  norm0 8995  norm-ii 9004  normsub 9008  norm3dif 9014  normpar 9021  normpar2 9023  polid2 9024  hhshsslem1 9137  projlem3 9188  projlem4 9189  pjthlem5 9223  pjthlem13 9231  shs0 9372  chj0 9378  pjoml2 9528  osumcor2 9590  pjsslem 9624  pjssm 9626  ho0sub 9721  hoaddsub 9747  hosd1 9748  hopncan 9750  hosubeq0 9752  hhblo 9828  hh0o 9829  nmop0 9910  nmfn0 9911  lnopunilem1 9935  lnophmlem2 9942  pjclem1 10123  pjcmmul1 10129  cvmd 10251  mdexch 10262  atabs 10328  dmdbr6at 10350  symgval 10403  cmpbva 10464  cmpran 10469  trnij 10637  stoi 10639  1cat 10692

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