Theorem 7p2e9 12425

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

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  2c2 12319  7c7 12324  8c8 12325  9c9 12326

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  df-8 12333  df-9 12334

This theorem is referenced by:  7p3e10  12806  7t7e49  12845  cos2bnd  16221  prmlem2  17154  139prm  17158  1259lem2  17166  1259lem3  17167  1259lem4  17168  1259lem5  17169  2503lem2  17172  4001lem4  17178  hgt750lem2  34646  aks4d1p1p7  42056  fmtno5lem4  47481  fmtno5fac  47507  139prmALT  47521