Metamath Proof Explorer


Theorem problem1

Description: Practice problem 1. Clues: 5p4e9 3p2e5 eqtri oveq1i . (Contributed by Filip Cernatescu, 16-Mar-2019) (Proof modification is discouraged.)

Ref Expression
Assertion problem1
|- ( ( 3 + 2 ) + 4 ) = 9

Proof

Step Hyp Ref Expression
1 3p2e5
 |-  ( 3 + 2 ) = 5
2 1 oveq1i
 |-  ( ( 3 + 2 ) + 4 ) = ( 5 + 4 )
3 5p4e9
 |-  ( 5 + 4 ) = 9
4 2 3 eqtri
 |-  ( ( 3 + 2 ) + 4 ) = 9