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 |
| 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 |