HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem 3eqtrrd 1559
Description: A deduction from three chained equalities.
Hypotheses
Ref Expression
3eqtrd.1 |- (ph -> A = B)
3eqtrd.2 |- (ph -> B = C)
3eqtrd.3 |- (ph -> C = D)
Assertion
Ref Expression
3eqtrrd |- (ph -> D = A)

Proof of Theorem 3eqtrrd
StepHypRef Expression
1 3eqtrd.3 . 2 |- (ph -> C = D)
2 3eqtrd.1 . . 3 |- (ph -> A = B)
3 3eqtrd.2 . . 3 |- (ph -> B = C)
42, 3eqtr2d 1555 . 2 |- (ph -> C = A)
51, 4eqtr3d 1556 1 |- (ph -> D = A)
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 997
This theorem is referenced by:  axcnre 5351  flmodOLD 6375  seq1seq02 6632  seqzp1 6637  expubnd 6697  subsq 6731  rereb 6866  sincossq 7552  abssinper 8795  nmbdoplbi 10032  nmcopexlem3 10036  nmcoplbi 10041  nmbdfnlbi 10061  nmcfnexlem3 10065  nmcfnlbi 10070  hstoh 10243
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504
This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515
Copyright terms: Public domain