HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem 2p2e4 8952
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
StepHypRef Expression
1 df-2 8920 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5364 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 8922 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 8921 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5363 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 8930 . . . 4  |-  2  e.  CC
7 ax-1cn 8204 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8246 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2085 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2084 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1517  (class class class)co 5353   1c1 8148    + caddc 8150   2c2 8911   3c3 8912   4c4 8913
This theorem is referenced by:  2t2e4  8980  i4  10187  ef01bndlem  11057  pythagtriplem1  11353  prmlem2  11603  43prm  11605  1259lem4  11614  2503lem1  11617  2503lem2  11618  2503lem3  11619  4001lem1  11621  4001lem4  11624  quart1lem  17751  log2ub  17845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-resscn 8203  ax-1cn 8204  ax-icn 8205  ax-addcl 8206  ax-addrcl 8207  ax-mulcl 8208  ax-mulrcl 8209  ax-addass 8211  ax-i2m1 8214  ax-1ne0 8215  ax-rrecex 8218  ax-cnre 8219
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 895  df-ex 1444  df-sb 1733  df-clab 2049  df-cleq 2054  df-clel 2057  df-ne 2181  df-ral 2275  df-rex 2276  df-rab 2278  df-v 2474  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-nul 3070  df-if 3178  df-sn 3257  df-pr 3258  df-op 3260  df-uni 3421  df-br 3583  df-opab 3637  df-xp 4266  df-cnv 4268  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fv 4280  df-ov 5356  df-2 8920  df-3 8921  df-4 8922
Copyright terms: Public domain