Theorem 4p3e7 12311

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 7380	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12247	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12237	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11102	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11160	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2755	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12230	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12310	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7379	. . 3 ⊢ ((4 + 2) + 1) = (6 + 1)
11	8, 10	eqtr4i 2755	. 2 ⊢ 7 = ((4 + 2) + 1)
12	7, 11	eqtr4i 2755	1 ⊢ (4 + 3) = 7

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104  ax-addass 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230

This theorem is referenced by:  4p4e8  12312  hash7g  14427  37prm  17067  317prm  17072  1259lem5  17081  2503lem2  17084  4001lem1  17087  4001lem2  17088  log2ub  26835  bposlem8  27178  2lgslem3d  27286  2lgsoddprmlem3d  27300  hgt750lem  34615  hgt750lem2  34616  fmtno5lem4  47530  257prm  47535  127prm  47573  gbpart7  47741  sbgoldbwt  47751  sbgoldbst  47752  ackval2012  48653