Theorem 4p3e7 12402

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 12312	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7424	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12333	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12323	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11195	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11253	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2760	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12316	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12401	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7423	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2760	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2760	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1539  (class class class)co 7413  1c1 11138   + caddc 11140  2c2 12303  3c3 12304  4c4 12305  6c6 12307  7c7 12308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11195  ax-addcl 11197  ax-addass 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316

This theorem is referenced by:  4p4e8  12403  hash7g  14508  37prm  17141  317prm  17146  1259lem5  17155  2503lem2  17158  4001lem1  17161  4001lem2  17162  log2ub  26929  bposlem8  27272  2lgslem3d  27380  2lgsoddprmlem3d  27394  hgt750lem  34641  hgt750lem2  34642  fmtno5lem4  47516  257prm  47521  127prm  47559  gbpart7  47727  sbgoldbwt  47737  sbgoldbst  47738  ackval2012  48585