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

Theorem 2p2e4 8942
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 8910 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5365 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 8912 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 8911 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5364 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 8920 . . . 4  |-  2  e.  CC
7 ax-1cn 8194 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8236 . . 3  |-  ( (
2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2106 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2105 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1536  (class class class)co 5354   1c1 8138    + caddc 8140   2c2 8901   3c3 8902   4c4 8903
This theorem is referenced by:  2t2e4  8970  i4  10172  ef01bndlem  11029  pythagtriplem1  11325  prmlem2  11575  43prm  11577  1259lem4  11586  2503lem1  11589  2503lem2  11590  2503lem3  11591  4001lem1  11593  4001lem4  11596  quart1lem  17660  log2ub  17754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-resscn 8193  ax-1cn 8194  ax-icn 8195  ax-addcl 8196  ax-addrcl 8197  ax-mulcl 8198  ax-mulrcl 8199  ax-addass 8201  ax-i2m1 8204  ax-1ne0 8205  ax-rrecex 8208  ax-cnre 8209
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 905  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-rab 2298  df-v 2494  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3089  df-if 3199  df-sn 3278  df-pr 3279  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-xp 4289  df-cnv 4291  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fv 4303  df-ov 5357  df-2 8910  df-3 8911  df-4 8912
Copyright terms: Public domain