Theorem 4p2e6 12324

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 12239	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7370	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12261	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11092	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11151	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2767	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12242	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7369	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2767	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12243	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2767	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1548  (class class class)co 7359  1c1 11035   + caddc 11037  2c2 12231  4c4 12233  5c5 12234  6c6 12235

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-addcl 11094  ax-addass 11099

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243

This theorem is referenced by:  4p3e7  12325  div4p1lem1div2  12427  4t4e16  12738  6gcd4e2  16502  2exp16  17056  163prm  17090  631prm  17092  1259lem4  17099  2503lem2  17103  2503lem3  17104  4001lem1  17106  4001lem2  17107  4001lem4  17109  bposlem9  27276  hgt750lem2  34846  3exp7  42551  3lexlogpow5ineq1  42552  aks4d1p1p5  42573  235t711  42795  ex-decpmul  42796  3cubeslem3r  43149  lhe4.4ex1a  44786  ceil5half3  47821  fmtno4prmfac  48062  fmtno5faclem1  48069  gbowgt5  48265  mogoldbb  48288