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 e. CC
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