Theorem 6p2e8 12362

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 12266	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7392	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12295	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11117	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11178	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2778	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12271	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7391	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2778	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12272	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2778	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1550  (class class class)co 7381  1c1 11060   + caddc 11062  2c2 12258  6c6 12262  7c7 12263  8c8 12264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-1cn 11117  ax-addcl 11119  ax-addass 11124

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-2 12266  df-3 12267  df-4 12268  df-5 12269  df-6 12270  df-7 12271  df-8 12272

This theorem is referenced by:  6p3e9  12363  6t3e18  12784  83prm  17131  1259lem2  17140  1259lem5  17143  2503lem2  17146  2503lem3  17147  4001lem1  17149  log2ub  26980  hgt750lem2  34893  3exp7  42608  3cubeslem3l  43205  resqrtvalex  44159  imsqrtvalex  44160  lhe4.4ex1a  44843  sin5tlem5  47409  fmtno5faclem3  48128