Theorem 3p2e5 12370

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 12282	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7423	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12300	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11174	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11231	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12284	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7422	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12285	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1540  (class class class)co 7412  1c1 11117   + caddc 11119  2c2 12274  3c3 12275  4c4 12276  5c5 12277

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-1cn 11174  ax-addcl 11176  ax-addass 11181

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  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 6495  df-fv 6551  df-ov 7415  df-2 12282  df-3 12283  df-4 12284  df-5 12285

This theorem is referenced by:  3p3e6  12371  2exp5  17026  2exp16  17031  prmlem1a  17047  5prm  17049  prmlem2  17060  1259lem1  17071  1259lem4  17074  1259prm  17076  4001lem1  17081  4001lem4  17084  birthday  26800  ppiub  27050  bposlem6  27135  bposlem9  27138  2lgsoddprmlem3d  27259  ex-mod  30135  cyc3conja  32752  fib5  33868  hgt750lem2  34128  kur14lem8  34668  problem1  35114  235t711  41668  3cubeslem3l  41887  3cubeslem3r  41888  fmtnorec2  46670  fmtno5lem4  46683  257prm  46688  fmtno4nprmfac193  46701  41prothprmlem2  46745  linevalexample  47238  ackval2012  47539  ackval3012  47540