Theorem 4p2e6 12398

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 12308	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7421	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12330	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11192	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11250	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12311	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7420	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12312	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1540  (class class class)co 7410  1c1 11135   + caddc 11137  2c2 12300  4c4 12302  5c5 12303  6c6 12304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-addcl 11194  ax-addass 11199

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312

This theorem is referenced by:  4p3e7  12399  div4p1lem1div2  12501  4t4e16  12812  6gcd4e2  16562  2exp16  17115  163prm  17149  631prm  17151  1259lem4  17158  2503lem2  17162  2503lem3  17163  4001lem1  17165  4001lem2  17166  4001lem4  17168  bposlem9  27260  hgt750lem2  34689  3exp7  42071  3lexlogpow5ineq1  42072  aks4d1p1p5  42093  235t711  42321  ex-decpmul  42322  3cubeslem3r  42677  lhe4.4ex1a  44320  ceil5half3  47336  fmtno4prmfac  47553  fmtno5faclem1  47560  gbowgt5  47743  mogoldbb  47766