Metamath Proof Explorer


Theorem 3p3e6

Description: 3 + 3 = 6. (Contributed by NM, 11-May-2004)

Ref Expression
Assertion 3p3e6 3 + 3 = 6

Proof

Step Hyp Ref Expression
1 df-3 3 = 2 + 1
2 1 oveq2i 3 + 3 = 3 + 2 + 1
3 3cn 3
4 2cn 2
5 ax-1cn 1
6 3 4 5 addassi 3 + 2 + 1 = 3 + 2 + 1
7 2 6 eqtr4i 3 + 3 = 3 + 2 + 1
8 df-6 6 = 5 + 1
9 3p2e5 3 + 2 = 5
10 9 oveq1i 3 + 2 + 1 = 5 + 1
11 8 10 eqtr4i 6 = 3 + 2 + 1
12 7 11 eqtr4i 3 + 3 = 6