Theorem 3p2e5 11360

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 11279	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 6802	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 11295	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 10194	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10248	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2796	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 11281	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 6801	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2796	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 11282	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2796	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1631  (class class class)co 6791  1c1 10137   + caddc 10139  2c2 11270  3c3 11271  4c4 11272  5c5 11273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-addass 10201  ax-i2m1 10204  ax-1ne0 10205  ax-rrecex 10208  ax-cnre 10209

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5992  df-fv 6037  df-ov 6794  df-2 11279  df-3 11280  df-4 11281  df-5 11282

This theorem is referenced by:  3p3e6  11361  2exp16  15997  prmlem1a  16013  5prm  16015  prmlem2  16027  1259lem1  16038  1259lem4  16041  1259prm  16043  4001lem1  16048  4001lem4  16051  birthday  24895  ppiub  25143  bposlem6  25228  bposlem9  25231  2lgsoddprmlem3d  25352  ex-mod  27641  fib5  30800  hgt750lem2  31063  kur14lem8  31526  problem1  31889  fmtnorec2  41976  fmtno5lem4  41989  257prm  41994  fmtno4nprmfac193  42007  2exp5  42028  41prothprmlem2  42056  linevalexample  42705