Theorem 4p2e6 12369

Description: 4 + 2 = 6. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
4p2e6	⊢ (4 + 2) = 6

Proof of Theorem 4p2e6

Step	Hyp	Ref	Expression
1		df-2 12279	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7422	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12301	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11170	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11228	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2763	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12282	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7421	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2763	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12283	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2763	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1541  (class class class)co 7411  1c1 11113   + caddc 11115  2c2 12271  4c4 12273  5c5 12274  6c6 12275

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 11170  ax-addcl 11172  ax-addass 11177

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283

This theorem is referenced by:  4p3e7  12370  div4p1lem1div2  12471  4t4e16  12780  6gcd4e2  16484  2exp16  17028  163prm  17062  631prm  17064  1259lem4  17071  2503lem2  17075  2503lem3  17076  4001lem1  17078  4001lem2  17079  4001lem4  17081  bposlem9  27019  hgt750lem2  33950  3exp7  41224  3lexlogpow5ineq1  41225  aks4d1p1p5  41246  235t711  41507  ex-decpmul  41508  3cubeslem3r  41727  lhe4.4ex1a  43390  fmtno4prmfac  46539  fmtno5faclem1  46546  gbowgt5  46729  mogoldbb  46752