Theorem 3eqtr4r 1498

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

Syntax hints:   = wceq 953

This theorem is referenced by:  dfin3 2237  difdifdir 2336  unipr 2505  iunrab 2586  unidif0 2729  dfdm4 3294  dmsnsnsn 3318  resres 3361  funopg 3533  1st2val 4079  2nd2val 4080  qsexg 4278  abfii2 4536  axmulass 5250  divmul13 5743  dfnn2 5884  3p2e5 5954  4p2e6 5956  5p2e7 5959  6p2e8 5963  7p2e9 5966  8p2e10 5968  halfpm6th 5979  nnesq 6592  sqrmuli 6634  cjcj 6713  recj 6717  imcj 6718  cjmul 6724  cjneg 6732  bcpasc2 6905  fnsmnt 7161  fsum0diag 7193  cos2bnd 7417  infmap2 7523  oprcn 7911  ipdirilem 8419  efghgrpilem 8634  dfrelog 8678  normlem2 8898  bcseq 8907  hilnorm 8951  pjthlem14 9147  cmcmlem 9451  fh3 9483  fh4 9484  spansnj 9508  pjadj 9535  lnophmlem2 9857  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