Theorem 7p2e9 12393

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 12295	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7410	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12326	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11179	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11237	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2760	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12301	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7409	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2760	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12302	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2760	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1539  (class class class)co 7399  1c1 11122   + caddc 11124  2c2 12287  7c7 12292  8c8 12293  9c9 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11179  ax-addcl 11181  ax-addass 11186

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402  df-2 12295  df-3 12296  df-4 12297  df-5 12298  df-6 12299  df-7 12300  df-8 12301  df-9 12302

This theorem is referenced by:  7p3e10  12775  7t7e49  12814  cos2bnd  16191  prmlem2  17124  139prm  17128  1259lem2  17136  1259lem3  17137  1259lem4  17138  1259lem5  17139  2503lem2  17142  4001lem4  17148  hgt750lem2  34605  aks4d1p1p7  42009  fmtno5lem4  47488  fmtno5fac  47514  139prmALT  47528