Theorem 5p2e7 12375

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 12282	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7423	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12307	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11174	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11231	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2762	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12286	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7422	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2762	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12287	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2762	1 ⊢ (5 + 2) = 7

Syntax hints:   = wceq 1540  (class class class)co 7412  1c1 11117   + caddc 11119  2c2 12274  5c5 12277  6c6 12278  7c7 12279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-1cn 11174  ax-addcl 11176  ax-addass 11181

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287

This theorem is referenced by:  5p3e8  12376  17prm  17057  prmlem2  17060  37prm  17061  317prm  17066  1259lem1  17071  1259lem2  17072  1259lem4  17074  2503lem2  17078  4001lem1  17081  4001lem4  17084  log2ub  26795  bposlem8  27137  aks4d1p1p4  41403  aks4d1p1p7  41406  ex-decpmul  41669  resqrtvalex  42859  imsqrtvalex  42860  fmtno5lem2  46681  257prm  46688  127prm  46726