Theorem 5p2e7 12413

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 12320	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7430	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12346	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11175	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11236	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2791	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12324	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7429	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2791	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12325	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2791	1 ⊢ (5 + 2) = 7

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11118   + caddc 11120  2c2 12312  5c5 12315  6c6 12316  7c7 12317

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177  ax-addass 11182

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325

This theorem is used by:  5p3e8  12414  17prm  17201  prmlem2  17204  37prm  17205  317prm  17210  1259lem1  17215  1259lem2  17216  1259lem4  17218  2503lem2  17222  4001lem1  17225  4001lem4  17228  log2ub  27167  bposlem8  27508  aks4d1p1p4  42898  aks4d1p1p7  42901  ex-decpmul  43127  resqrtvalex  44431  imsqrtvalex  44432  fmtno5lem2  48366  257prm  48373  127prm  48411