Theorem 4p3e7 12418

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 12328	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7442	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12349	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12339	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11211	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11269	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2766	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12332	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12417	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7441	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2766	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2766	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  2c2 12319  3c3 12320  4c4 12321  6c6 12323  7c7 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213  ax-addass 11218

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332

This theorem is referenced by:  4p4e8  12419  hash7g  14522  37prm  17155  317prm  17160  1259lem5  17169  2503lem2  17172  4001lem1  17175  4001lem2  17176  log2ub  27007  bposlem8  27350  2lgslem3d  27458  2lgsoddprmlem3d  27472  hgt750lem  34645  hgt750lem2  34646  fmtno5lem4  47481  257prm  47486  127prm  47524  gbpart7  47692  sbgoldbwt  47702  sbgoldbst  47703  ackval2012  48541