Metamath Proof Explorer


Theorem 3eqtr4ri

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Hypotheses 3eqtr4i.1 A = B
3eqtr4i.2 C = A
3eqtr4i.3 D = B
Assertion 3eqtr4ri D = C

Proof

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