Theorem 3p2e5 12362

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

Assertion

Ref	Expression
3p2e5	⊢ (3 + 2) = 5

Proof of Theorem 3p2e5

Step	Hyp	Ref	Expression
1		df-2 12274	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7402	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12293	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11125	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11186	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2787	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12276	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7401	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2787	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12277	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2787	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1559  (class class class)co 7391  1c1 11068   + caddc 11070  2c2 12266  3c3 12267  4c4 12268  5c5 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-addcl 11127  ax-addass 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-2 12274  df-3 12275  df-4 12276  df-5 12277

This theorem is referenced by:  3p3e6  12363  fz0to5un2tp  13630  2exp5  17112  2exp16  17117  prmlem1a  17133  5prm  17135  prmlem2  17147  1259lem1  17158  1259lem4  17161  1259prm  17163  4001lem1  17168  4001lem4  17171  birthday  27007  ppiub  27256  bposlem6  27341  bposlem9  27344  2lgsoddprmlem3d  27465  ex-mod  30608  cyc3conja  33298  fib5  34663  hgt750lem2  34907  kur14lem8  35524  problem1  35976  235t711  42875  3cubeslem3l  43228  3cubeslem3r  43229  sin5tlem1  47428  sin5tlem5  47432  sin5t  47433  goldrasin  47437  fmtnorec2  48113  fmtno5lem4  48126  257prm  48131  fmtno4nprmfac193  48144  41prothprmlem2  48188  linevalexample  48978  ackval2012  49274  ackval3012  49275