Theorem 3p2e5 12282

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 12199	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7366	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12217	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11075	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11133	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2759	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12201	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7365	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2759	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12202	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2759	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1541  (class class class)co 7355  1c1 11018   + caddc 11020  2c2 12191  3c3 12192  4c4 12193  5c5 12194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075  ax-addcl 11077  ax-addass 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-2 12199  df-3 12200  df-4 12201  df-5 12202

This theorem is referenced by:  3p3e6  12283  fz0to5un2tp  13538  2exp5  17004  2exp16  17009  prmlem1a  17025  5prm  17027  prmlem2  17038  1259lem1  17049  1259lem4  17052  1259prm  17054  4001lem1  17059  4001lem4  17062  birthday  26911  ppiub  27162  bposlem6  27247  bposlem9  27250  2lgsoddprmlem3d  27371  ex-mod  30450  cyc3conja  33167  fib5  34490  hgt750lem2  34737  kur14lem8  35329  problem1  35781  235t711  42475  3cubeslem3l  42843  3cubeslem3r  42844  fmtnorec2  47705  fmtno5lem4  47718  257prm  47723  fmtno4nprmfac193  47736  41prothprmlem2  47780  linevalexample  48557  ackval2012  48853  ackval3012  48854