Theorem 5p2e7 12420

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 12327	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7442	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12352	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11211	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11269	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2766	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12331	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7441	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2766	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12332	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2766	1 ⊢ (5 + 2) = 7

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  2c2 12319  5c5 12322  6c6 12323  7c7 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213  ax-addass 11218

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332

This theorem is referenced by:  5p3e8  12421  17prm  17151  prmlem2  17154  37prm  17155  317prm  17160  1259lem1  17165  1259lem2  17166  1259lem4  17168  2503lem2  17172  4001lem1  17175  4001lem4  17178  log2ub  27007  bposlem8  27350  aks4d1p1p4  42053  aks4d1p1p7  42056  ex-decpmul  42319  resqrtvalex  43635  imsqrtvalex  43636  fmtno5lem2  47479  257prm  47486  127prm  47524