Theorem 2p2e4 10817

Description: Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2p2e4	⊢ (2 + 2) = 4

Proof of Theorem 2p2e4

Step	Hyp	Ref	Expression
1		df-2 10757	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 6374	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 10759	. . 3 ⊢ 4 = (3 + 1)
4		df-3 10758	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 6373	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 10769	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 9682	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 9736	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2531	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2530	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1468  (class class class)co 6363  1c1 9625   + caddc 9627  2c2 10748  3c3 10749  4c4 10750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-addass 9689  ax-i2m1 9692  ax-1ne0 9693  ax-rrecex 9696  ax-cnre 9697

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366  df-2 10757  df-3 10758  df-4 10759

This theorem is referenced by:  2t2e4  10849  i4  12491  4bc2eq6  12628  bpoly4  14272  fsumcube  14273  ef01bndlem  14398  6gcd4e2  14664  pythagtriplem1  14928  prmlem2  15252  43prm  15254  1259lem4  15266  2503lem1  15269  2503lem2  15270  2503lem3  15271  4001lem1  15273  4001lem4  15276  quart1lem  23942  log2ub  24036  wallispi2lem1  38369  stirlinglem8  38379  sqwvfourb  38529  gbogt5  39383  gbpart7  39388  sgoldbaltlem1  39400  sgoldbalt  39402  nnsum3primes4  39403  3exp4mod41  39436  2t6m3t4e0  41319  2p2ne5  41724