Theorem 4p3e7 12269

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 12184	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7352	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12205	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12195	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11059	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11117	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2757	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12188	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12268	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7351	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2757	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2757	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1541  (class class class)co 7341  1c1 11002   + caddc 11004  2c2 12175  3c3 12176  4c4 12177  6c6 12179  7c7 12180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11059  ax-addcl 11061  ax-addass 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188

This theorem is referenced by:  4p4e8  12270  hash7g  14388  37prm  17027  317prm  17032  1259lem5  17041  2503lem2  17044  4001lem1  17047  4001lem2  17048  log2ub  26881  bposlem8  27224  2lgslem3d  27332  2lgsoddprmlem3d  27346  hgt750lem  34656  hgt750lem2  34657  fmtno5lem4  47587  257prm  47592  127prm  47630  gbpart7  47798  sbgoldbwt  47808  sbgoldbst  47809  ackval2012  48723