Theorem 3p2e5 12402

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 12314	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7427	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12333	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11169	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11230	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2791	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12316	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7426	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2791	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12317	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2791	1 ⊢ (3 + 2) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416  1c1 11112   + caddc 11114  2c2 12306  3c3 12307  4c4 12308  5c5 12309

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11169  ax-addcl 11171  ax-addass 11176

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-2 12314  df-3 12315  df-4 12316  df-5 12317

This theorem is used by:  3p3e6  12403  fz0to5un2tp  13671  2exp5  17162  2exp16  17167  prmlem1a  17183  5prm  17185  prmlem2  17197  1259lem1  17208  1259lem4  17211  1259prm  17213  4001lem1  17218  4001lem4  17221  birthday  27148  ppiub  27397  bposlem6  27482  bposlem9  27485  2lgsoddprmlem3d  27606  ex-mod  30829  cyc3conja  33500  fib5  34819  hgt750lem2  35063  kur14lem8  35718  problem1  36170  235t711  43099  3cubeslem3l  43450  3cubeslem3r  43451  sin5tlem1  47643  sin5tlem5  47647  sin5t  47648  goldrasin  47652  fmtnorec2  48328  fmtno5lem4  48341  257prm  48346  fmtno4nprmfac193  48359  41prothprmlem2  48403  linevalexample  49208  ackval2012  49504  ackval3012  49505