Theorem 3p2e5 12292

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 12209	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7364	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12227	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11086	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11144	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2755	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12211	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7363	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2755	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12212	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2755	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1540  (class class class)co 7353  1c1 11029   + caddc 11031  2c2 12201  3c3 12202  4c4 12203  5c5 12204

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 11086  ax-addcl 11088  ax-addass 11093

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-2 12209  df-3 12210  df-4 12211  df-5 12212

This theorem is referenced by:  3p3e6  12293  fz0to5un2tp  13552  2exp5  17015  2exp16  17020  prmlem1a  17036  5prm  17038  prmlem2  17049  1259lem1  17060  1259lem4  17063  1259prm  17065  4001lem1  17070  4001lem4  17073  birthday  26880  ppiub  27131  bposlem6  27216  bposlem9  27219  2lgsoddprmlem3d  27340  ex-mod  30411  cyc3conja  33112  fib5  34375  hgt750lem2  34622  kur14lem8  35188  problem1  35640  235t711  42281  3cubeslem3l  42662  3cubeslem3r  42663  fmtnorec2  47531  fmtno5lem4  47544  257prm  47549  fmtno4nprmfac193  47562  41prothprmlem2  47606  linevalexample  48384  ackval2012  48680  ackval3012  48681