MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2p2e4 Unicode version

Theorem 2p2e4 9232
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 9195 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5381 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9197 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9196 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5380 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9207 . . . 4  |-  2  e.  CC
7 ax-1cn 8225 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8275 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2093 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2092 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1524  (class class class)co 5370   1c1 8169    + caddc 8171   2c2 9186   3c3 9187   4c4 9188
This theorem is referenced by:  2t2e4  9261  i4  10578  ef01bndlem  11667  pythagtriplem1  11994  prmlem2  12245  43prm  12247  1259lem4  12256  2503lem1  12259  2503lem2  12260  2503lem3  12261  4001lem1  12263  4001lem4  12266  quart1lem  18726  log2ub  18820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594  ax-16 1780  ax-ext 2051  ax-resscn 8224  ax-1cn 8225  ax-icn 8226  ax-addcl 8227  ax-addrcl 8228  ax-mulcl 8229  ax-mulrcl 8230  ax-addass 8232  ax-i2m1 8235  ax-1ne0 8236  ax-rrecex 8239  ax-cnre 8240
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1451  df-sb 1741  df-clab 2057  df-cleq 2062  df-clel 2065  df-ne 2189  df-ral 2283  df-rex 2284  df-rab 2286  df-v 2482  df-dif 2801  df-un 2803  df-in 2805  df-ss 2809  df-nul 3078  df-if 3187  df-sn 3266  df-pr 3267  df-op 3269  df-uni 3435  df-br 3597  df-opab 3651  df-xp 4280  df-cnv 4282  df-dm 4284  df-rn 4285  df-res 4286  df-ima 4287  df-fv 4294  df-ov 5373  df-2 9195  df-3 9196  df-4 9197
  Copyright terms: Public domain W3C validator