Theorem 3p2e5 11946

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 11858	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7202	. . . 4 ⊢ (3 + 2) = (3 + (1 + 1))
3		3cn 11876	. . . . 5 ⊢ 3 ∈ ℂ
4		ax-1cn 10752	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10808	. . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (3 + 2) = ((3 + 1) + 1)
7		df-4 11860	. . . 4 ⊢ 4 = (3 + 1)
8	7	oveq1i 7201	. . 3 ⊢ (4 + 1) = ((3 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (3 + 2) = (4 + 1)
10		df-5 11861	. 2 ⊢ 5 = (4 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (3 + 2) = 5

Syntax hints:   = wceq 1543  (class class class)co 7191  1c1 10695   + caddc 10697  2c2 11850  3c3 11851  4c4 11852  5c5 11853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-addcl 10754  ax-addass 10759

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-2 11858  df-3 11859  df-4 11860  df-5 11861

This theorem is referenced by:  3p3e6  11947  2exp5  16602  2exp16  16607  prmlem1a  16623  5prm  16625  prmlem2  16636  1259lem1  16647  1259lem4  16650  1259prm  16652  4001lem1  16657  4001lem4  16660  birthday  25791  ppiub  26039  bposlem6  26124  bposlem9  26127  2lgsoddprmlem3d  26248  ex-mod  28486  cyc3conja  31097  fib5  32038  hgt750lem2  32298  kur14lem8  32842  problem1  33290  235t711  39967  3cubeslem3l  40152  3cubeslem3r  40153  fmtnorec2  44611  fmtno5lem4  44624  257prm  44629  fmtno4nprmfac193  44642  41prothprmlem2  44686  linevalexample  45352  ackval2012  45653  ackval3012  45654