Description: 7 + 7 = 14. (Contributed by Mario Carneiro, 19Apr2015)
Ref  Expression  

Assertion  7p7e14   ( 7 + 7 ) = ; 1 4 
Step  Hyp  Ref  Expression 

1  7nn0   7 e. NN0 

2  6nn0   6 e. NN0 

3  3nn0   3 e. NN0 

4  df7   7 = ( 6 + 1 ) 

5  df4   4 = ( 3 + 1 ) 

6  7p6e13   ( 7 + 6 ) = ; 1 3 

7  1 2 3 4 5 6  6p5lem   ( 7 + 7 ) = ; 1 4 