Theorem 3p2e5 12493

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 12405	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12424	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11258	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11319	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2786	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12407	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7430	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2786	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12408	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2786	1 ⊢ (3 + 2) = 5

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420  1c1 11201   + caddc 11203  2c2 12397  3c3 12398  4c4 12399  5c5 12400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11258  ax-addcl 11260  ax-addass 11265

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408

This theorem is used by:  3p3e6  12494  fz0to5un2tp  13765  2exp5  17263  2exp16  17268  prmlem1a  17284  5prm  17286  prmlem2  17298  1259lem1  17309  1259lem4  17312  1259prm  17314  4001lem1  17319  4001lem4  17322  birthday  27282  ppiub  27531  bposlem6  27616  bposlem9  27619  2lgsoddprmlem3d  27740  ex-mod  31050  cyc3conja  33718  fib5  35037  hgt750lem2  35281  kur14lem8  35978  problem1  36430  2p3e5  43317  2p5e7  43319  3p4e7  43322  3p5e8  43323  235t711  43363  3cubeslem3l  43697  3cubeslem3r  43698  sin5tlem1  47919  sin5tlem5  47923  sin5t  47924  goldrasin  47929  fmtnorec2  48628  fmtno5lem4  48641  257prm  48646  fmtno4nprmfac193  48659  41prothprmlem2  48703  linevalexample  49507  ackval2012  49803  ackval3012  49804