Theorem 3p2e5 12327

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 12244	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7378	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12262	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11096	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11155	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12246	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7377	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12247	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  2c2 12236  3c3 12237  4c4 12238  5c5 12239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098  ax-addass 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247

This theorem is referenced by:  3p3e6  12328  fz0to5un2tp  13585  2exp5  17056  2exp16  17061  prmlem1a  17077  5prm  17079  prmlem2  17090  1259lem1  17101  1259lem4  17104  1259prm  17106  4001lem1  17111  4001lem4  17114  birthday  26918  ppiub  27167  bposlem6  27252  bposlem9  27255  2lgsoddprmlem3d  27376  ex-mod  30519  cyc3conja  33218  fib5  34549  hgt750lem2  34796  kur14lem8  35395  problem1  35847  235t711  42737  3cubeslem3l  43118  3cubeslem3r  43119  sin5tlem1  47321  sin5tlem5  47325  sin5t  47326  goldrasin  47330  fmtnorec2  48006  fmtno5lem4  48019  257prm  48024  fmtno4nprmfac193  48037  41prothprmlem2  48081  linevalexample  48871  ackval2012  49167  ackval3012  49168