Theorem 7p7e14

Description: 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		7nn0	⊢ 7 ∈ ℕ0
2		6nn0	⊢ 6 ∈ ℕ0
3		3nn0	⊢ 3 ∈ ℕ0
4		df-7	⊢ 7 = ( 6 + 1 )
5		df-4	⊢ 4 = ( 3 + 1 )
6		7p6e13	⊢ ( 7 + 6 ) = ; 1 3
7	1 2 3 4 5 6	6p5lem	⊢ ( 7 + 7 ) = ; 1 4