Theorem 4p2e6 12417

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 12327	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7442	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12349	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11211	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11269	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2766	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12330	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7441	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2766	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12331	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2766	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  2c2 12319  4c4 12321  5c5 12322  6c6 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213  ax-addass 11218

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331

This theorem is referenced by:  4p3e7  12418  div4p1lem1div2  12519  4t4e16  12830  6gcd4e2  16572  2exp16  17125  163prm  17159  631prm  17161  1259lem4  17168  2503lem2  17172  2503lem3  17173  4001lem1  17175  4001lem2  17176  4001lem4  17178  bposlem9  27351  hgt750lem2  34646  3exp7  42035  3lexlogpow5ineq1  42036  aks4d1p1p5  42057  235t711  42318  ex-decpmul  42319  3cubeslem3r  42675  lhe4.4ex1a  44325  ceil5half3  47280  fmtno4prmfac  47497  fmtno5faclem1  47504  gbowgt5  47687  mogoldbb  47710