Theorem 3p2e5 11596

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 11501	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 6985	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 11519	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 10391	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10448	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2798	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 11503	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 6984	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2798	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 11504	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2798	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1508  (class class class)co 6974  1c1 10334   + caddc 10336  2c2 11493  3c3 11494  4c4 11495  5c5 11496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-1cn 10391  ax-addcl 10393  ax-addass 10398

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-rex 3087  df-rab 3090  df-v 3410  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-2 11501  df-3 11502  df-4 11503  df-5 11504

This theorem is referenced by:  3p3e6  11597  2exp16  16278  prmlem1a  16294  5prm  16296  prmlem2  16307  1259lem1  16318  1259lem4  16321  1259prm  16323  4001lem1  16328  4001lem4  16331  birthday  25249  ppiub  25497  bposlem6  25582  bposlem9  25585  2lgsoddprmlem3d  25706  ex-mod  28021  fib5  31341  hgt750lem2  31603  kur14lem8  32082  problem1  32465  235t711  38647  fmtnorec2  43107  fmtno5lem4  43120  257prm  43125  fmtno4nprmfac193  43138  2exp5  43157  41prothprmlem2  43185  linevalexample  43851