Theorem 4p3e7 12489

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 12399	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7429	. . 3 ⊢ (4 + 3) = (4 + (2 + 1))
3		4cn 12421	. . . 4 ⊢ 4 ∈ ℂ
4		2cn 12411	. . . 4 ⊢ 2 ∈ ℂ
5		ax-1cn 11251	. . . 4 ⊢ 1 ∈ ℂ
6	3, 4, 5	addassi 11312	. . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1))
7	2, 6	eqtr4i 2787	. 2 ⊢ (4 + 3) = ((4 + 2) + 1)
8		df-7 12403	. . 3 ⊢ 7 = (6 + 1)
9		4p2e6 12488	. . . 4 ⊢ (4 + 2) = 6
10	9	oveq1i 7428	. . 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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  2c2 12390  3c3 12391  4c4 12392  6c6 12394  7c7 12395

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addcl 11253  ax-addass 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403

This theorem is used by:  4p4e8  12490  hash7g  14624  37prm  17292  317prm  17297  1259lem5  17306  2503lem2  17309  4001lem1  17312  4001lem2  17313  log2ub  27270  bposlem8  27611  2lgslem3d  27719  2lgsoddprmlem3d  27733  hgt750lem  35273  hgt750lem2  35274  fmtno5lem4  48610  257prm  48615  127prm  48653  ppivalnn4  48681  gbpart7  48834  sbgoldbwt  48844  sbgoldbst  48845  ackval2012  49772