Theorem 6p2e8 12404

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 12308	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7430	. . . 4 ⊢ (6 + 2) = (6 + (1 + 1))
3		6cn 12336	. . . . 5 ⊢ 6 ∈ ℂ
4		ax-1cn 11198	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11256	. . . 4 ⊢ ((6 + 1) + 1) = (6 + (1 + 1))
6	2, 5	eqtr4i 2756	. . 3 ⊢ (6 + 2) = ((6 + 1) + 1)
7		df-7 12313	. . . 4 ⊢ 7 = (6 + 1)
8	7	oveq1i 7429	. . 3 ⊢ (7 + 1) = ((6 + 1) + 1)
9	6, 8	eqtr4i 2756	. 2 ⊢ (6 + 2) = (7 + 1)
10		df-8 12314	. 2 ⊢ 8 = (7 + 1)
11	9, 10	eqtr4i 2756	1 ⊢ (6 + 2) = 8

Syntax hints:   = wceq 1533  (class class class)co 7419  1c1 11141   + caddc 11143  2c2 12300  6c6 12304  7c7 12305  8c8 12306

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 2696  ax-1cn 11198  ax-addcl 11200  ax-addass 11205

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314

This theorem is referenced by:  6p3e9  12405  6t3e18  12815  83prm  17095  1259lem2  17104  1259lem5  17107  2503lem2  17110  2503lem3  17111  4001lem1  17113  log2ub  26926  hgt750lem2  34415  3exp7  41656  3cubeslem3l  42248  resqrtvalex  43217  imsqrtvalex  43218  lhe4.4ex1a  43908  fmtno5faclem3  47058