Theorem 4p2e6 12031

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 11941	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7263	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 11963	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 10835	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10891	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2770	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 11944	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7262	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2770	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 11945	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2770	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   + caddc 10780  2c2 11933  4c4 11935  5c5 11936  6c6 11937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10835  ax-addcl 10837  ax-addass 10842

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6373  df-fv 6423  df-ov 7255  df-2 11941  df-3 11942  df-4 11943  df-5 11944  df-6 11945

This theorem is referenced by:  4p3e7  12032  div4p1lem1div2  12133  4t4e16  12440  6gcd4e2  16149  2exp16  16695  163prm  16729  631prm  16731  1259lem4  16738  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem2  16746  4001lem4  16748  bposlem9  26320  hgt750lem2  32507  3exp7  39968  3lexlogpow5ineq1  39969  aks4d1p1p5  39989  235t711  40212  ex-decpmul  40213  3cubeslem3r  40397  lhe4.4ex1a  41809  fmtno4prmfac  44885  fmtno5faclem1  44892  gbowgt5  45075  mogoldbb  45098