Theorem 3p2e5 12414

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 12326	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7441	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12344	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11210	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11268	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2765	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12328	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7440	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2765	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12329	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2765	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   + caddc 11155  2c2 12318  3c3 12319  4c4 12320  5c5 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212  ax-addass 11217

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328  df-5 12329

This theorem is referenced by:  3p3e6  12415  fz0to5un2tp  13667  2exp5  17119  2exp16  17124  prmlem1a  17140  5prm  17142  prmlem2  17153  1259lem1  17164  1259lem4  17167  1259prm  17169  4001lem1  17174  4001lem4  17177  birthday  27011  ppiub  27262  bposlem6  27347  bposlem9  27350  2lgsoddprmlem3d  27471  ex-mod  30477  cyc3conja  33159  fib5  34386  hgt750lem2  34645  kur14lem8  35197  problem1  35649  235t711  42317  3cubeslem3l  42673  3cubeslem3r  42674  fmtnorec2  47467  fmtno5lem4  47480  257prm  47485  fmtno4nprmfac193  47498  41prothprmlem2  47542  linevalexample  48240  ackval2012  48540  ackval3012  48541