Theorem 6p2e8 12367

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 12271	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7416	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12299	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11164	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11220	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2763	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12276	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7415	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2763	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12277	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2763	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1541  (class class class)co 7405  1c1 11107   + caddc 11109  2c2 12263  6c6 12267  7c7 12268  8c8 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addcl 11166  ax-addass 11171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277

This theorem is referenced by:  6p3e9  12368  6t3e18  12778  83prm  17052  1259lem2  17061  1259lem5  17064  2503lem2  17067  2503lem3  17068  4001lem1  17070  log2ub  26443  hgt750lem2  33652  3exp7  40906  3cubeslem3l  41409  resqrtvalex  42381  imsqrtvalex  42382  lhe4.4ex1a  43073  fmtno5faclem3  46235