Theorem 7p2e9 12513

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

Assertion

Ref	Expression
7p2e9	⊢ (7 + 2) = 9

Proof of Theorem 7p2e9

Step	Hyp	Ref	Expression
1		df-2 12415	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7438	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12447	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11268	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11329	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12421	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7437	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12422	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (7 + 2) = 9

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7427  1c1 11211   + caddc 11213  2c2 12407  7c7 12412  8c8 12413  9c9 12414

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  df-8 12421  df-9 12422

This theorem is used by:  7p3e10  12904  7t7e49  12943  cos2bnd  16368  prmlem2  17310  139prm  17314  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  2503lem2  17328  4001lem4  17334  hgt750lem2  35334  aks4d1p1p7  43264  2p7e9  43460  fmtno5lem4  48780  fmtno5fac  48806  139prmALT  48820