Theorem 3p2e5 12360

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 12272	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7417	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12290	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11165	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11221	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2764	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12274	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7416	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2764	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12275	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2764	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1542  (class class class)co 7406  1c1 11108   + caddc 11110  2c2 12264  3c3 12265  4c4 12266  5c5 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-addcl 11167  ax-addass 11172

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-2 12272  df-3 12273  df-4 12274  df-5 12275

This theorem is referenced by:  3p3e6  12361  2exp5  17016  2exp16  17021  prmlem1a  17037  5prm  17039  prmlem2  17050  1259lem1  17061  1259lem4  17064  1259prm  17066  4001lem1  17071  4001lem4  17074  birthday  26449  ppiub  26697  bposlem6  26782  bposlem9  26785  2lgsoddprmlem3d  26906  ex-mod  29692  cyc3conja  32304  fib5  33393  hgt750lem2  33653  kur14lem8  34193  problem1  34639  235t711  41201  3cubeslem3l  41410  3cubeslem3r  41411  fmtnorec2  46198  fmtno5lem4  46211  257prm  46216  fmtno4nprmfac193  46229  41prothprmlem2  46273  linevalexample  47030  ackval2012  47331  ackval3012  47332