Metamath Proof Explorer


Theorem 4p3e7

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

Ref Expression
Assertion 4p3e7 4+3=7

Proof

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