Theorem 3eqtr4r 1506

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
3eqtr4r	|- D = C

Proof of Theorem 3eqtr4r

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	eqtr2 1496	1 |- D = C

Syntax hints:   = wceq 956

This theorem is referenced by:  dfin3 2247  difdifdir 2346  unipr 2515  iunrab 2596  unidif0 2739  dfdm4 3305  dmsnsnsn 3329  resres 3377  unidmrn 3516  funopg 3547  1st2val 4095  2nd2val 4096  qsexg 4294  abfii2OLD 4562  axmulass 5278  divmul13 5787  dfnn2 5936  3p2e5 6007  4p2e6 6009  5p2e7 6012  6p2e8 6016  7p2e9 6019  8p2e10 6021  halfpm6th 6032  nnesq 6662  sqrmuli 6704  cjcj 6778  recj 6782  imcj 6783  cjmul 6789  cjneg 6797  bcpasc2 6967  fnsmnt 7226  fsum0diag 7258  cos2bnd 7475  infmap2 7581  oprcn 7977  ipdirilem 8488  efghgrpilem 8719  dfrelog 8756  normlem2 8977  bcseq 8986  hilnorm 9030  pjthlem14 9232  cmcmlem 9534  fh3 9566  fh4 9567  spansnj 9591  pjadj 9618  lnophmlem2 9942  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