Theorem 3p2e5 10749

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 10675	. . . . 5 |- 2 = ( 1 + 1 )
2	1	oveq2i 6306	. . . 4 |- ( 3 + 2 ) = ( 3 + ( 1 + 1 ) )
3		3cn 10691	. . . . 5 |- 3 e. CC
4		ax-1cn 9602	. . . . 5 |- 1 e. CC
5	3, 4, 4	addassi 9656	. . . 4 |- ( ( 3 + 1 ) + 1 ) = ( 3 + ( 1 + 1 ) )
6	2, 5	eqtr4i 2478	. . 3 |- ( 3 + 2 ) = ( ( 3 + 1 ) + 1 )
7		df-4 10677	. . . 4 |- 4 = ( 3 + 1 )
8	7	oveq1i 6305	. . 3 |- ( 4 + 1 ) = ( ( 3 + 1 ) + 1 )
9	6, 8	eqtr4i 2478	. 2 |- ( 3 + 2 ) = ( 4 + 1 )
10		df-5 10678	. 2 |- 5 = ( 4 + 1 )
11	9, 10	eqtr4i 2478	1 |- ( 3 + 2 ) = 5

Syntax hints:   = wceq 1446  (class class class)co 6295   1c1 9545   + caddc 9547   2c2 10666   3c3 10667   4c4 10668   5c5 10669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-addass 9609  ax-i2m1 9612  ax-1ne0 9613  ax-rrecex 9616  ax-cnre 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-iota 5549  df-fv 5593  df-ov 6298  df-2 10675  df-3 10676  df-4 10677  df-5 10678

This theorem is referenced by:  3p3e6  10750  2exp16  15073  prmlem1a  15090  5prm  15092  prmlem2  15103  1259lem1  15114  1259lem4  15117  1259prm  15119  4001lem1  15124  4001lem4  15127  birthday  23892  ppiub  24144  bposlem6  24229  bposlem9  24232  fib5  29250  kur14lem8  29948  problem1  30309  41prothprmlem2  38928  linevalexample  40292