Theorem 7p2e9 12369

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 12271	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7416	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12302	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11164	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11220	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2763	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12277	. . . 4 ⊢ 8 = (7 + 1)
8	7	oveq1i 7415	. . 3 ⊢ (8 + 1) = ((7 + 1) + 1)
9	6, 8	eqtr4i 2763	. 2 ⊢ (7 + 2) = (8 + 1)
10		df-9 12278	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2763	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1541  (class class class)co 7405  1c1 11107   + caddc 11109  2c2 12263  7c7 12268  8c8 12269  9c9 12270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addcl 11166  ax-addass 11171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278

This theorem is referenced by:  7p3e10  12748  7t7e49  12787  cos2bnd  16127  prmlem2  17049  139prm  17053  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem2  17067  4001lem4  17073  hgt750lem2  33652  aks4d1p1p7  40927  fmtno5lem4  46210  fmtno5fac  46236  139prmALT  46250