Theorem 3p2e5 12415

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 12327	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7424	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 12346	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 11182	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11243	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2786	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 12329	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7423	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2786	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 12330	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2786	1 ⊢ (3 + 2) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413  1c1 11125   + caddc 11127  2c2 12319  3c3 12320  4c4 12321  5c5 12322

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 2732  ax-1cn 11182  ax-addcl 11184  ax-addass 11189

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7416  df-2 12327  df-3 12328  df-4 12329  df-5 12330

This theorem is used by:  3p3e6  12416  fz0to5un2tp  13686  2exp5  17177  2exp16  17182  prmlem1a  17198  5prm  17200  prmlem2  17212  1259lem1  17223  1259lem4  17226  1259prm  17228  4001lem1  17233  4001lem4  17236  birthday  27191  ppiub  27440  bposlem6  27525  bposlem9  27528  2lgsoddprmlem3d  27649  ex-mod  30929  cyc3conja  33597  fib5  34916  hgt750lem2  35160  kur14lem8  35792  problem1  36244  2p3e5  43132  2p5e7  43134  3p4e7  43137  3p5e8  43138  235t711  43180  3cubeslem3l  43531  3cubeslem3r  43532  sin5tlem1  47737  sin5tlem5  47741  sin5t  47742  goldrasin  47747  fmtnorec2  48446  fmtno5lem4  48459  257prm  48464  fmtno4nprmfac193  48477  41prothprmlem2  48521  linevalexample  49325  ackval2012  49621  ackval3012  49622