Theorem 4p3e7 12319

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 12234	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7369	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12255	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12245	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11085	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11144	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2763	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12238	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12318	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7368	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2763	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2763	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1542  (class class class)co 7358  1c1 11028   + caddc 11030  2c2 12225  3c3 12226  4c4 12227  6c6 12229  7c7 12230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11085  ax-addcl 11087  ax-addass 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-2 12233  df-3 12234  df-4 12235  df-5 12236  df-6 12237  df-7 12238

This theorem is referenced by:  4p4e8  12320  hash7g  14437  37prm  17080  317prm  17085  1259lem5  17094  2503lem2  17097  4001lem1  17100  4001lem2  17101  log2ub  26924  bposlem8  27266  2lgslem3d  27374  2lgsoddprmlem3d  27388  hgt750lem  34809  hgt750lem2  34810  fmtno5lem4  48021  257prm  48026  127prm  48064  ppivalnn4  48092  gbpart7  48245  sbgoldbwt  48255  sbgoldbst  48256  ackval2012  49169