Theorem 7p2e9 12372

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 12274	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7413	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12305	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11165	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11223	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2755	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12280	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7412	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2755	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12281	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2755	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1533  (class class class)co 7402  1c1 11108   + caddc 11110  2c2 12266  7c7 12271  8c8 12272  9c9 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-1cn 11165  ax-addcl 11167  ax-addass 11172

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281

This theorem is referenced by:  7p3e10  12751  7t7e49  12790  cos2bnd  16134  prmlem2  17058  139prm  17062  1259lem2  17070  1259lem3  17071  1259lem4  17072  1259lem5  17073  2503lem2  17076  4001lem4  17082  hgt750lem2  34182  aks4d1p1p7  41445  fmtno5lem4  46769  fmtno5fac  46795  139prmALT  46809