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