Theorem 6p2e8 12370

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 12274	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7413	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12302	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11165	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11223	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2755	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12279	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7412	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2755	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12280	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2755	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1533  (class class class)co 7402  1c1 11108   + caddc 11110  2c2 12266  6c6 12270  7c7 12271  8c8 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-1cn 11165  ax-addcl 11167  ax-addass 11172

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280

This theorem is referenced by:  6p3e9  12371  6t3e18  12781  83prm  17061  1259lem2  17070  1259lem5  17073  2503lem2  17076  2503lem3  17077  4001lem1  17079  log2ub  26821  hgt750lem2  34182  3exp7  41424  3cubeslem3l  41974  resqrtvalex  42945  imsqrtvalex  42946  lhe4.4ex1a  43637  fmtno5faclem3  46794