Theorem 3p6e9

Description: 3 + 6 = 9. (Contributed by SN, 24-Aug-2026)

	Ref	Expression
Assertion	3p6e9	⊢ ( 3 + 6 ) = 9

Proof

Step	Hyp	Ref	Expression
1		3cn	⊢ 3 ∈ ℂ
2	1 1 1	addassi	⊢ ( ( 3 + 3 ) + 3 ) = ( 3 + ( 3 + 3 ) )
3		3p3e6	⊢ ( 3 + 3 ) = 6
4	3	oveq1i	⊢ ( ( 3 + 3 ) + 3 ) = ( 6 + 3 )
5		6p3e9	⊢ ( 6 + 3 ) = 9
6	4 5	eqtri	⊢ ( ( 3 + 3 ) + 3 ) = 9
7	3	oveq2i	⊢ ( 3 + ( 3 + 3 ) ) = ( 3 + 6 )
8	2 6 7	3eqtr3ri	⊢ ( 3 + 6 ) = 9