Theorem 5p2e7 12508

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 12415	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7438	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12441	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11268	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11329	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12419	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7437	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12420	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (5 + 2) = 7

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7427  1c1 11211   + caddc 11213  2c2 12407  5c5 12410  6c6 12411  7c7 12412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270  ax-addass 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420

This theorem is used by:  5p3e8  12509  17prm  17307  prmlem2  17310  37prm  17311  317prm  17316  1259lem1  17321  1259lem2  17322  1259lem4  17324  2503lem2  17328  4001lem1  17331  4001lem4  17334  log2ub  27289  bposlem8  27630  aks4d1p1p4  43261  aks4d1p1p7  43264  2p5e7  43458  2p7e9  43460  3p4e7  43461  ex-decpmul  43503  resqrtvalex  44785  imsqrtvalex  44786  fmtno5lem2  48778  257prm  48785  127prm  48823