Theorem 7p2e9 12404

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 12306	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. . . 4 ⊢ (7 + 2) = (7 + (1 + 1))
3		7cn 12337	. . . . 5 ⊢ 7 ∈ ℂ
4		ax-1cn 11197	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11255	. . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1))
6	2, 5	eqtr4i 2759	. . 3 ⊢ (7 + 2) = ((7 + 1) + 1)
7		df-8 12312	. . . 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 12313	. 2 ⊢ 9 = (8 + 1)
11	9, 10	eqtr4i 2759	1 ⊢ (7 + 2) = 9

Syntax hints:   = wceq 1534  (class class class)co 7420  1c1 11140   + caddc 11142  2c2 12298  7c7 12303  8c8 12304  9c9 12305

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 11197  ax-addcl 11199  ax-addass 11204

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 12306  df-3 12307  df-4 12308  df-5 12309  df-6 12310  df-7 12311  df-8 12312  df-9 12313

This theorem is referenced by:  7p3e10  12783  7t7e49  12822  cos2bnd  16165  prmlem2  17089  139prm  17093  1259lem2  17101  1259lem3  17102  1259lem4  17103  1259lem5  17104  2503lem2  17107  4001lem4  17113  hgt750lem2  34284  aks4d1p1p7  41545  fmtno5lem4  46896  fmtno5fac  46922  139prmALT  46936