Theorem 3p2e5 12417

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 12329	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7442	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12347	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11213	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11271	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2768	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12331	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7441	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2768	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12332	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2768	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  2c2 12321  3c3 12322  4c4 12323  5c5 12324

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215  ax-addass 11220

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332

This theorem is referenced by:  3p3e6  12418  fz0to5un2tp  13671  2exp5  17123  2exp16  17128  prmlem1a  17144  5prm  17146  prmlem2  17157  1259lem1  17168  1259lem4  17171  1259prm  17173  4001lem1  17178  4001lem4  17181  birthday  26997  ppiub  27248  bposlem6  27333  bposlem9  27336  2lgsoddprmlem3d  27457  ex-mod  30468  cyc3conja  33177  fib5  34407  hgt750lem2  34667  kur14lem8  35218  problem1  35670  235t711  42339  3cubeslem3l  42697  3cubeslem3r  42698  fmtnorec2  47530  fmtno5lem4  47543  257prm  47548  fmtno4nprmfac193  47561  41prothprmlem2  47605  linevalexample  48312  ackval2012  48612  ackval3012  48613