Theorem 5p2e7 12396

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 12303	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7422	. . . 4 ⊢ (5 + 2) = (5 + (1 + 1))
3		5cn 12329	. . . . 5 ⊢ 5 ∈ ℂ
4		ax-1cn 11158	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11219	. . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1))
6	2, 5	eqtr4i 2795	. . 3 ⊢ (5 + 2) = ((5 + 1) + 1)
7		df-6 12307	. . . 4 ⊢ 6 = (5 + 1)
8	7	oveq1i 7421	. . 3 ⊢ (6 + 1) = ((5 + 1) + 1)
9	6, 8	eqtr4i 2795	. 2 ⊢ (5 + 2) = (6 + 1)
10		df-7 12308	. 2 ⊢ 7 = (6 + 1)
11	9, 10	eqtr4i 2795	1 ⊢ (5 + 2) = 7

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103  2c2 12295  5c5 12298  6c6 12299  7c7 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addcl 11160  ax-addass 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308

This theorem is referenced by:  5p3e8  12397  17prm  17177  prmlem2  17180  37prm  17181  317prm  17186  1259lem1  17191  1259lem2  17192  1259lem4  17194  2503lem2  17198  4001lem1  17201  4001lem4  17204  log2ub  27080  bposlem8  27421  aks4d1p1p4  42728  aks4d1p1p7  42731  ex-decpmul  42957  resqrtvalex  44263  imsqrtvalex  44264  fmtno5lem2  48195  257prm  48202  127prm  48240