Theorem 4p3e7 12496

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 12406	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7431	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12428	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12418	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11258	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11319	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2786	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12410	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12495	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7430	. . 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 7420  1c1 11201   + caddc 11203  2c2 12397  3c3 12398  4c4 12399  6c6 12401  7c7 12402

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 11258  ax-addcl 11260  ax-addass 11265

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 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410

This theorem is used by:  4p4e8  12497  hash7g  14631  37prm  17299  317prm  17304  1259lem5  17313  2503lem2  17316  4001lem1  17319  4001lem2  17320  log2ub  27277  bposlem8  27618  2lgslem3d  27726  2lgsoddprmlem3d  27740  hgt750lem  35280  hgt750lem2  35281  fmtno5lem4  48641  257prm  48646  127prm  48684  ppivalnn4  48712  gbpart7  48865  sbgoldbwt  48875  sbgoldbst  48876  ackval2012  49803