Theorem 5p2e7 12179

Description: 5 + 2 = 7. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
5p2e7	⊢ (5 + 2) = 7

Proof of Theorem 5p2e7

Step	Hyp	Ref	Expression
1		df-2 12086	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7318	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12111	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 10979	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11035	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2767	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12090	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7317	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2767	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12091	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2767	1 ⊢ (5 + 2) = 7

Syntax hints:   = wceq 1539  (class class class)co 7307  1c1 10922   + caddc 10924  2c2 12078  5c5 12081  6c6 12082  7c7 12083

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-1cn 10979  ax-addcl 10981  ax-addass 10986

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-2 12086  df-3 12087  df-4 12088  df-5 12089  df-6 12090  df-7 12091

This theorem is referenced by:  5p3e8  12180  17prm  16867  prmlem2  16870  37prm  16871  317prm  16876  1259lem1  16881  1259lem2  16882  1259lem4  16884  2503lem2  16888  4001lem1  16891  4001lem4  16894  log2ub  26148  bposlem8  26488  aks4d1p1p4  40279  aks4d1p1p7  40282  ex-decpmul  40515  resqrtvalex  41466  imsqrtvalex  41467  fmtno5lem2  45250  257prm  45257  127prm  45295