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

Theorem 2p2e4 8962
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 8930 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5367 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 8932 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 8931 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5366 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 8940 . . . 4  |-  2  e.  CC
7 ax-1cn 8210 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8252 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2086 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2085 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1518  (class class class)co 5356   1c1 8154    + caddc 8156   2c2 8921   3c3 8922   4c4 8923
This theorem is referenced by:  2t2e4  8990  i4  10211  ef01bndlem  11116  pythagtriplem1  11441  prmlem2  11691  43prm  11693  1259lem4  11702  2503lem1  11705  2503lem2  11706  2503lem3  11707  4001lem1  11709  4001lem4  11712  quart1lem  18103  log2ub  18197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-resscn 8209  ax-1cn 8210  ax-icn 8211  ax-addcl 8212  ax-addrcl 8213  ax-mulcl 8214  ax-mulrcl 8215  ax-addass 8217  ax-i2m1 8220  ax-1ne0 8221  ax-rrecex 8224  ax-cnre 8225
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 896  df-ex 1445  df-sb 1734  df-clab 2050  df-cleq 2055  df-clel 2058  df-ne 2182  df-ral 2276  df-rex 2277  df-rab 2279  df-v 2475  df-dif 2794  df-un 2796  df-in 2798  df-ss 2802  df-nul 3071  df-if 3180  df-sn 3259  df-pr 3260  df-op 3262  df-uni 3423  df-br 3585  df-opab 3639  df-xp 4268  df-cnv 4270  df-dm 4272  df-rn 4273  df-res 4274  df-ima 4275  df-fv 4282  df-ov 5359  df-2 8930  df-3 8931  df-4 8932
Copyright terms: Public domain