Theorem 4p2e6 12495

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

Assertion

Ref	Expression
4p2e6	⊢ (4 + 2) = 6

Proof of Theorem 4p2e6

Step	Hyp	Ref	Expression
1		df-2 12405	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12428	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11258	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11319	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2787	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12408	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7430	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2787	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12409	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2787	1 ⊢ (4 + 2) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203  2c2 12397  4c4 12399  5c5 12400  6c6 12401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260  ax-addass 11265

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409

This theorem is used by:  4p3e7  12496  div4p1lem1div2  12601  4t4e16  12918  6gcd4e2  16711  2exp16  17268  163prm  17303  631prm  17305  1259lem4  17312  2503lem2  17316  2503lem3  17317  4001lem1  17319  4001lem2  17320  4001lem4  17322  bposlem9  27619  hgt750lem2  35281  3exp7  43103  3lexlogpow5ineq1  43104  aks4d1p1p5  43125  4p4e8ALT  43309  2p4e6  43317  235t711  43362  ex-decpmul  43363  3cubeslem3r  43697  lhe4.4ex1a  45312  ceil5half3  48415  fmtno4prmfac  48656  fmtno5faclem1  48663  gbowgt5  48859  mogoldbb  48882