Theorem 3eqtr4ri 1923

Description: An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4ri	|- D = C

Proof of Theorem 3eqtr4ri

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

Syntax hints:   = wceq 1298

This theorem is referenced by:  dfin3 2834  difdifdir 2957  unipr 3191  iunrab 3299  unidif0 3476  dfdm4 4151  dmun 4163  resres 4228  inres 4233  cnvun 4322  dmsnsnsn 4371  coundi 4396  coundir 4398  unidmrn 4420  funopg 4454  1st2val 5038  2nd2val 5039  df1st2 5068  df2nd2 5069  oeoalem 5271  qsexg 5352  abfii2 5652  axmulass 6431  negnegi 6549  divmul13i 6964  dfnn2 7119  3p2e5 7191  4p2e6 7193  5p2e7 7196  6p2e8 7200  7p2e9 7203  8p2e10 7205  halfpm6th 7218  nnesqi 7912  sqrmulii 7954  cjcji 8028  recji 8032  imcji 8033  cjmuli 8039  cjnegi 8047  bcpasc2i 8219  arisumi 8487  fsum0diag 8520  cos2bnd 8741  infmap2 8850  oprcn 9255  ipdirilem 9829  efghgrpilem 10073  dfrelog 10110  normlem2 10610  bcseqi 10619  hilnormi 10663  pjthlem14 10865  cmcmlem 11167  fh3i 11199  fh4i 11200  spansnji 11226  pjadjii 11253  lnophmlem2 11579  predidm 13899  dfom5 14081  cnvtr 15016  ufcondr 15581  cncfres 15895  cnresoprab 15915  pcoass 16085  stb2strx 16747  stb3strx 16754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain