Theorem 3p2e5 12332

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 12249	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7398	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12267	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11126	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11184	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2755	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12251	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7397	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2755	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12252	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2755	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  2c2 12241  3c3 12242  4c4 12243  5c5 12244

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128  ax-addass 11133

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252

This theorem is referenced by:  3p3e6  12333  fz0to5un2tp  13592  2exp5  17056  2exp16  17061  prmlem1a  17077  5prm  17079  prmlem2  17090  1259lem1  17101  1259lem4  17104  1259prm  17106  4001lem1  17111  4001lem4  17114  birthday  26864  ppiub  27115  bposlem6  27200  bposlem9  27203  2lgsoddprmlem3d  27324  ex-mod  30378  cyc3conja  33114  fib5  34396  hgt750lem2  34643  kur14lem8  35200  problem1  35652  235t711  42293  3cubeslem3l  42674  3cubeslem3r  42675  fmtnorec2  47544  fmtno5lem4  47557  257prm  47562  fmtno4nprmfac193  47575  41prothprmlem2  47619  linevalexample  48384  ackval2012  48680  ackval3012  48681