Theorem 4p3e7 12501

Description: 4 + 3 = 7. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
4p3e7	⊢ (4 + 3) = 7

Proof of Theorem 4p3e7

Step	Hyp	Ref	Expression
1		df-3 12411	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7433	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12433	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12423	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11263	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11324	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2786	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12415	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12500	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7432	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2786	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2786	1 ⊢ (4 + 3) = 7

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7422  1c1 11206   + caddc 11208  2c2 12402  3c3 12403  4c4 12404  6c6 12406  7c7 12407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11263  ax-addcl 11265  ax-addass 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549  df-ov 7425  df-2 12410  df-3 12411  df-4 12412  df-5 12413  df-6 12414  df-7 12415

This theorem is used by:  4p4e8  12502  hash7g  14636  37prm  17306  317prm  17311  1259lem5  17320  2503lem2  17323  4001lem1  17326  4001lem2  17327  log2ub  27284  bposlem8  27625  2lgslem3d  27733  2lgsoddprmlem3d  27747  hgt750lem  35328  hgt750lem2  35329  fmtno5lem4  48748  257prm  48753  127prm  48791  ppivalnn4  48819  gbpart7  48972  sbgoldbwt  48982  sbgoldbst  48983  ackval2012  49910