Theorem 4p3e7 12409

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 12319	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7430	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12341	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12331	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11173	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11234	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2791	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12323	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12408	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7429	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2791	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2791	1 ⊢ (4 + 3) = 7

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11116   + caddc 11118  2c2 12310  3c3 12311  4c4 12312  6c6 12314  7c7 12315

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-addcl 11175  ax-addass 11180

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12318  df-3 12319  df-4 12320  df-5 12321  df-6 12322  df-7 12323

This theorem is used by:  4p4e8  12410  hash7g  14541  37prm  17203  317prm  17208  1259lem5  17217  2503lem2  17220  4001lem1  17223  4001lem2  17224  log2ub  27165  bposlem8  27506  2lgslem3d  27614  2lgsoddprmlem3d  27628  hgt750lem  35103  hgt750lem2  35104  fmtno5lem4  48366  257prm  48371  127prm  48409  ppivalnn4  48437  gbpart7  48590  sbgoldbwt  48600  sbgoldbst  48601  ackval2012  49528