Metamath Proof Explorer


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