Theorem 3p2e5 12392

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 12304	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7423	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12323	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11159	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11220	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12306	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7422	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12307	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1570  (class class class)co 7412  1c1 11102   + caddc 11104  2c2 12296  3c3 12297  4c4 12298  5c5 12299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addcl 11161  ax-addass 11166

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-2 12304  df-3 12305  df-4 12306  df-5 12307

This theorem is referenced by:  3p3e6  12393  fz0to5un2tp  13661  2exp5  17146  2exp16  17151  prmlem1a  17167  5prm  17169  prmlem2  17181  1259lem1  17192  1259lem4  17195  1259prm  17197  4001lem1  17202  4001lem4  17205  birthday  27100  ppiub  27349  bposlem6  27434  bposlem9  27437  2lgsoddprmlem3d  27558  ex-mod  30781  cyc3conja  33458  fib5  34776  hgt750lem2  35020  kur14lem8  35686  problem1  36138  235t711  43047  3cubeslem3l  43400  3cubeslem3r  43401  sin5tlem1  47593  sin5tlem5  47597  sin5t  47598  goldrasin  47602  fmtnorec2  48278  fmtno5lem4  48291  257prm  48296  fmtno4nprmfac193  48309  41prothprmlem2  48353  linevalexample  49158  ackval2012  49454  ackval3012  49455