Theorem 7p2e9 12403

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 12305	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12336	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11196	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11254	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2759	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12311	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7430	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2759	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12312	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2759	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1534  (class class class)co 7420  1c1 11139   + caddc 11141  2c2 12297  7c7 12302  8c8 12303  9c9 12304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11196  ax-addcl 11198  ax-addass 11203

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312

This theorem is referenced by:  7p3e10  12782  7t7e49  12821  cos2bnd  16164  prmlem2  17088  139prm  17092  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  2503lem2  17106  4001lem4  17112  hgt750lem2  34284  aks4d1p1p7  41545  fmtno5lem4  46896  fmtno5fac  46922  139prmALT  46936