Theorem 3p2e5 12486

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 12398	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7429	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12417	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11251	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11312	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2787	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12400	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7428	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2787	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12401	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2787	1 ⊢ (3 + 2) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  2c2 12390  3c3 12391  4c4 12392  5c5 12393

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addcl 11253  ax-addass 11258

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-2 12398  df-3 12399  df-4 12400  df-5 12401

This theorem is used by:  3p3e6  12487  fz0to5un2tp  13758  2exp5  17256  2exp16  17261  prmlem1a  17277  5prm  17279  prmlem2  17291  1259lem1  17302  1259lem4  17305  1259prm  17307  4001lem1  17312  4001lem4  17315  birthday  27275  ppiub  27524  bposlem6  27609  bposlem9  27612  2lgsoddprmlem3d  27733  ex-mod  31043  cyc3conja  33711  fib5  35030  hgt750lem2  35274  kur14lem8  35957  problem1  36409  2p3e5  43296  2p5e7  43298  3p4e7  43301  3p5e8  43302  235t711  43342  3cubeslem3l  43676  3cubeslem3r  43677  sin5tlem1  47888  sin5tlem5  47892  sin5t  47893  goldrasin  47898  fmtnorec2  48597  fmtno5lem4  48610  257prm  48615  fmtno4nprmfac193  48628  41prothprmlem2  48672  linevalexample  49476  ackval2012  49772  ackval3012  49773