Theorem 4p3e7 12316

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 12226	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7373	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12247	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12237	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11118	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11174	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2762	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12230	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12315	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7372	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2762	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2762	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1541  (class class class)co 7362  1c1 11061   + caddc 11063  2c2 12217  3c3 12218  4c4 12219  6c6 12221  7c7 12222

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-addcl 11120  ax-addass 11125

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230

This theorem is referenced by:  4p4e8  12317  37prm  17004  317prm  17009  1259lem5  17018  2503lem2  17021  4001lem1  17024  4001lem2  17025  log2ub  26336  bposlem8  26676  2lgslem3d  26784  2lgsoddprmlem3d  26798  hgt750lem  33353  hgt750lem2  33354  fmtno5lem4  45868  257prm  45873  127prm  45911  gbpart7  46079  sbgoldbwt  46089  sbgoldbst  46090  ackval2012  46897