Theorem 7p2e9 12543

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 12445	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7462	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12477	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11297	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11358	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12451	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7461	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12452	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (7 + 2) = 9

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  7c7 12442  8c8 12443  9c9 12444

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299  ax-addass 11304

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452

This theorem is used by:  7p3e10  12934  7t7e49  12973  cos2bnd  16400  prmlem2  17342  139prm  17346  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem2  17360  4001lem4  17366  hgt750lem2  35392  aks4d1p1p7  43390  2p7e9  43586  fmtno5lem4  48914  fmtno5fac  48940  139prmALT  48954