Theorem 4p2e6 12502

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 12412	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12435	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11265	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11326	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2786	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12415	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7434	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2786	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12416	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2786	1 ⊢ (4 + 2) = 6

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424  1c1 11208   + caddc 11210  2c2 12404  4c4 12406  5c5 12407  6c6 12408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-addcl 11267  ax-addass 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413  df-4 12414  df-5 12415  df-6 12416

This theorem is used by:  4p3e7  12503  div4p1lem1div2  12608  4t4e16  12925  6gcd4e2  16720  2exp16  17277  163prm  17312  631prm  17314  1259lem4  17321  2503lem2  17325  2503lem3  17326  4001lem1  17328  4001lem2  17329  4001lem4  17331  bposlem9  27628  hgt750lem2  35331  3exp7  43240  3lexlogpow5ineq1  43241  aks4d1p1p5  43262  4p4e8ALT  43446  2p4e6  43454  235t711  43499  ex-decpmul  43500  3cubeslem3r  43834  lhe4.4ex1a  45450  ceil5half3  48552  fmtno4prmfac  48793  fmtno5faclem1  48800  gbowgt5  48996  mogoldbb  49019