Theorem 3p2e5 11791

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 11703	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7170	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 11721	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 10598	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10654	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2850	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 11705	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7169	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2850	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 11706	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2850	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1536  (class class class)co 7159  1c1 10541   + caddc 10543  2c2 11695  3c3 11696  4c4 11697  5c5 11698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-1cn 10598  ax-addcl 10600  ax-addass 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-2 11703  df-3 11704  df-4 11705  df-5 11706

This theorem is referenced by:  3p3e6  11792  2exp16  16427  prmlem1a  16443  5prm  16445  prmlem2  16456  1259lem1  16467  1259lem4  16470  1259prm  16472  4001lem1  16477  4001lem4  16480  birthday  25535  ppiub  25783  bposlem6  25868  bposlem9  25871  2lgsoddprmlem3d  25992  ex-mod  28231  cyc3conja  30803  fib5  31667  hgt750lem2  31927  kur14lem8  32464  problem1  32912  235t711  39183  3cubeslem3l  39289  3cubeslem3r  39290  fmtnorec2  43712  fmtno5lem4  43725  257prm  43730  fmtno4nprmfac193  43743  2exp5  43762  41prothprmlem2  43790  linevalexample  44457