Theorem 3eqtr 1123

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 1119	. 2 ⊢ B = D
5	1, 4	eqtr 1119	1 ⊢ A = D

Syntax hints:   = wceq 1091

This theorem is referenced by:  dfrab2 1696  difin0 1759  undifv 1760  undif1 1761  undif2 1762  difun2 1763  difdifdir 1765  unop 1931  unisn 1932  unidif0 1944  intsn 1991  op1stb 1992  unisuc 2299  xpun 2463  dfrn2 2523  dfdmf 2526  dfrnf 2561  res0 2578  resopab 2598  dfima2 2604  imai 2613  ima0 2615  resdisj 2656  tz7.44-1 2966  dmoprab 3031  rnoprab 3033  f1stres 3096  df1o2 3111  df2o2 3112  ecid 3236  qsid 3237  sbthlem5 3353  dfsdom2 3362  mapenlem2 3385  rankpr 3536  scottexs 3543  scott0s 3544  kmlem3 3582  hta 3619  cda0en 3720  supsrlem2 4020  axmulass 4073  axi2m1 4082  subneg 4148  subeq0 4163  muladd 4181  mulneg1 4190  mulneg2 4191  mul2neg 4192  negdi2 4194  divrec 4236  div23 4244  rec11i 4261  ltsubadd 4316  ltneg 4330  prodgt0i 4387  ltmul1i 4393  nnsub 4450  2p2e4 4488  3t3e9 4505  crulem 4528  crmult 4530  seq1lem 4668  cu2 4711  binom 4712  discrlem1 4713  nnesq 4720  sqr0 4730  sqrlem11 4741  sqrlem16 4746  cjcj 4808  ipcn 4820  addcj 4828  abslem2i 4866  facnnt 4870  fac0 4871  ruclem6 4890  ruclem7 4891  ruclem12 4896  ruclem15 4899  infmap2lem1 4951  hvnegdi 5034  hvsubeq0 5035  hvsubcan2 5036  hvaddcan 5037  hvsubadd 5038  normlem0 5062  normlem1 5063  normlem3 5065  normlem8 5071  bcseq 5073  norm0 5079  norm-ii 5086  normsub 5089  norm3dif 5094  normpar 5099  normpar2 5100  projlem3 5195  projlem4 5196  pjthlem5 5229  pjthlem13 5237  chj0 5377  pjoml2 5495  fh1 5518  fh2 5519  pjsslem 5570  pjssm 5572  hods0 5620  hosd 5622  hosd1 5623  pjclem1 5649

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org