Theorem 6p2e8 12401

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 12305	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12333	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11196	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11254	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2759	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12310	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7430	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2759	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12311	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2759	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1534  (class class class)co 7420  1c1 11139   + caddc 11141  2c2 12297  6c6 12301  7c7 12302  8c8 12303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11196  ax-addcl 11198  ax-addass 11203

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311

This theorem is referenced by:  6p3e9  12402  6t3e18  12812  83prm  17091  1259lem2  17100  1259lem5  17103  2503lem2  17106  2503lem3  17107  4001lem1  17109  log2ub  26880  hgt750lem2  34284  3exp7  41524  3cubeslem3l  42106  resqrtvalex  43075  imsqrtvalex  43076  lhe4.4ex1a  43766  fmtno5faclem3  46921