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

Theorem 2p2e4 9214
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 9182 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5371 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9184 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9183 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5370 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9192 . . . 4  |-  2  e.  CC
7 ax-1cn 8215 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8263 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2088 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2087 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1520  (class class class)co 5360   1c1 8159    + caddc 8161   2c2 9173   3c3 9174   4c4 9175
This theorem is referenced by:  2t2e4  9242  i4  10559  ef01bndlem  11647  pythagtriplem1  11974  prmlem2  12225  43prm  12227  1259lem4  12236  2503lem1  12239  2503lem2  12240  2503lem3  12241  4001lem1  12243  4001lem4  12246  quart1lem  18705  log2ub  18799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-resscn 8214  ax-1cn 8215  ax-icn 8216  ax-addcl 8217  ax-addrcl 8218  ax-mulcl 8219  ax-mulrcl 8220  ax-addass 8222  ax-i2m1 8225  ax-1ne0 8226  ax-rrecex 8229  ax-cnre 8230
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1736  df-clab 2052  df-cleq 2057  df-clel 2060  df-ne 2184  df-ral 2278  df-rex 2279  df-rab 2281  df-v 2477  df-dif 2796  df-un 2798  df-in 2800  df-ss 2804  df-nul 3073  df-if 3182  df-sn 3261  df-pr 3262  df-op 3264  df-uni 3425  df-br 3587  df-opab 3641  df-xp 4270  df-cnv 4272  df-dm 4274  df-rn 4275  df-res 4276  df-ima 4277  df-fv 4284  df-ov 5363  df-2 9182  df-3 9183  df-4 9184
Copyright terms: Public domain