Theorem 2p2e4 9266

Description: Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpegif/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 9229	. . 3 |- 2 = ( 1 + 1 )
2	1	oveq2i 5415	. 2 |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) )
3		df-4 9231	. . 3 |- 4 = ( 3 + 1 )
4		df-3 9230	. . . 4 |- 3 = ( 2 + 1 )
5	4	oveq1i 5414	. . 3 |- ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
6		2cn 9241	. . . 4 |- 2 e. CC
7		ax-1cn 8259	. . . 4 |- 1 e. CC
8	6, 7, 7	addassi 8309	. . 3 |- ( ( 2 + 1 ) + 1 ) = ( 2 + ( 1 + 1 ) )
9	3, 5, 8	3eqtri 2124	. 2 |- 4 = ( 2 + ( 1 + 1 ) )
10	2, 9	eqtr4i 2123	1 |- ( 2 + 2 ) = 4

Syntax hints:   = wceq 1531  (class class class)co 5404   1c1 8203   + caddc 8205   2c2 9220   3c3 9221   4c4 9222

This theorem is referenced by:  2t2e4  9295  i4  10612  ef01bndlem  11701  pythagtriplem1  12028  prmlem2  12279  43prm  12281  1259lem4  12290  2503lem1  12293  2503lem2  12294  2503lem3  12295  4001lem1  12297  4001lem4  12300  quart1lem  18760  log2ub  18854

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-resscn 8258  ax-1cn 8259  ax-icn 8260  ax-addcl 8261  ax-addrcl 8262  ax-mulcl 8263  ax-mulrcl 8264  ax-addass 8266  ax-i2m1 8269  ax-1ne0 8270  ax-rrecex 8273  ax-cnre 8274

This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 902  df-ex 1457  df-sb 1748  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-rab 2318  df-v 2514  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-nul 3111  df-if 3221  df-sn 3300  df-pr 3301  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-xp 4314  df-cnv 4316  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fv 4328  df-ov 5407  df-2 9229  df-3 9230  df-4 9231