Theorem 5p2e7 12318

Description: 5 + 2 = 7. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
5p2e7	⊢ (5 + 2) = 7

Proof of Theorem 5p2e7

Step	Hyp	Ref	Expression
1		df-2 12225	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7373	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12250	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11118	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11174	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12229	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7372	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12230	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (5 + 2) = 7

Syntax hints:   = wceq 1541  (class class class)co 7362  1c1 11061   + caddc 11063  2c2 12217  5c5 12220  6c6 12221  7c7 12222

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 2702  ax-1cn 11118  ax-addcl 11120  ax-addass 11125

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 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230

This theorem is referenced by:  5p3e8  12319  17prm  17000  prmlem2  17003  37prm  17004  317prm  17009  1259lem1  17014  1259lem2  17015  1259lem4  17017  2503lem2  17021  4001lem1  17024  4001lem4  17027  log2ub  26336  bposlem8  26676  aks4d1p1p4  40601  aks4d1p1p7  40604  ex-decpmul  40864  resqrtvalex  42039  imsqrtvalex  42040  fmtno5lem2  45866  257prm  45873  127prm  45911