Theorem 6p2e8 12508

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

Assertion

Ref	Expression
6p2e8	⊢ (6 + 2) = 8

Proof of Theorem 6p2e8

Step	Hyp	Ref	Expression
1		df-2 12412	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12441	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11265	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11326	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2786	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12417	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7434	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2786	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12418	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2786	1 ⊢ (6 + 2) = 8

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424  1c1 11208   + caddc 11210  2c2 12404  6c6 12408  7c7 12409  8c8 12410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-addcl 11267  ax-addass 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413  df-4 12414  df-5 12415  df-6 12416  df-7 12417  df-8 12418

This theorem is used by:  6p3e9  12509  6t3e18  12931  83prm  17310  1259lem2  17319  1259lem5  17322  2503lem2  17325  2503lem3  17326  4001lem1  17328  log2ub  27286  hgt750lem2  35331  3exp7  43240  4p4e8ALT  43446  3cubeslem3l  43833  resqrtvalex  44782  imsqrtvalex  44783  lhe4.4ex1a  45450  sin5tlem5  48059  fmtno5faclem3  48802