Theorem 7p2e9 12332

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 12239	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7371	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12270	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11091	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11150	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2767	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12245	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7370	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2767	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12246	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2767	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1548  (class class class)co 7360  1c1 11034   + caddc 11036  2c2 12231  7c7 12236  8c8 12237  9c9 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11091  ax-addcl 11093  ax-addass 11098

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246

This theorem is referenced by:  7p3e10  12714  7t7e49  12753  cos2bnd  16150  prmlem2  17085  139prm  17089  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  2503lem2  17103  4001lem4  17109  hgt750lem2  34848  aks4d1p1p7  42574  fmtno5lem4  48048  fmtno5fac  48074  139prmALT  48088