Theorem 6p2e8 12397

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 12301	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7414	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12329	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11185	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11243	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2761	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12306	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7413	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2761	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12307	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2761	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  2c2 12293  6c6 12297  7c7 12298  8c8 12299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187  ax-addass 11192

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307

This theorem is referenced by:  6p3e9  12398  6t3e18  12811  83prm  17140  1259lem2  17149  1259lem5  17152  2503lem2  17155  2503lem3  17156  4001lem1  17158  log2ub  26909  hgt750lem2  34630  3exp7  42012  3cubeslem3l  42656  resqrtvalex  43616  imsqrtvalex  43617  lhe4.4ex1a  44301  fmtno5faclem3  47543