Theorem 4p3e7 12365

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 12275	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7402	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12297	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12287	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11125	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11186	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2787	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12279	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12364	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7401	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2787	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2787	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1559  (class class class)co 7391  1c1 11068   + caddc 11070  2c2 12266  3c3 12267  4c4 12268  6c6 12270  7c7 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-addcl 11127  ax-addass 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279

This theorem is referenced by:  4p4e8  12366  hash7g  14493  37prm  17148  317prm  17153  1259lem5  17162  2503lem2  17165  4001lem1  17168  4001lem2  17169  log2ub  27002  bposlem8  27343  2lgslem3d  27451  2lgsoddprmlem3d  27465  hgt750lem  34906  hgt750lem2  34907  fmtno5lem4  48126  257prm  48131  127prm  48169  ppivalnn4  48197  gbpart7  48350  sbgoldbwt  48360  sbgoldbst  48361  ackval2012  49274