Metamath Proof Explorer


Theorem 6p3e9

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

Ref Expression
Assertion 6p3e9 6+3=9

Proof

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