This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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