Theorem 3p2e5 12533

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 12445	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7462	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12464	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11297	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11358	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12447	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7461	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12448	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (3 + 2) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  3c3 12438  4c4 12439  5c5 12440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299  ax-addass 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448

This theorem is used by:  3p3e6  12534  fz0to5un2tp  13805  2exp5  17307  2exp16  17312  prmlem1a  17328  5prm  17330  prmlem2  17342  1259lem1  17353  1259lem4  17356  1259prm  17358  4001lem1  17363  4001lem4  17366  birthday  27339  ppiub  27588  bposlem6  27673  bposlem9  27676  2lgsoddprmlem3d  27797  ex-mod  31107  cyc3conja  33817  fib5  35148  hgt750lem2  35392  kur14lem8  36186  problem1  36638  2p3e5  43582  2p5e7  43584  3p4e7  43587  3p5e8  43588  235t711  43628  3cubeslem3l  43962  3cubeslem3r  43963  sin5tlem1  48192  sin5tlem5  48196  sin5t  48197  goldrasin  48202  fmtnorec2  48901  fmtno5lem4  48914  257prm  48919  fmtno4nprmfac193  48932  41prothprmlem2  48976  linevalexample  49838  ackval2012  50134  ackval3012  50135