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

Theorem 2p2e4 9228
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 9191 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5377 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9193 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9192 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5376 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9203 . . . 4  |-  2  e.  CC
7 ax-1cn 8221 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8271 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2089 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2088 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1520  (class class class)co 5366   1c1 8165    + caddc 8167   2c2 9182   3c3 9183   4c4 9184
This theorem is referenced by:  2t2e4  9257  i4  10574  ef01bndlem  11663  pythagtriplem1  11990  prmlem2  12241  43prm  12243  1259lem4  12252  2503lem1  12255  2503lem2  12256  2503lem3  12257  4001lem1  12259  4001lem4  12262  quart1lem  18722  log2ub  18816
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 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-resscn 8220  ax-1cn 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-mulrcl 8226  ax-addass 8228  ax-i2m1 8231  ax-1ne0 8232  ax-rrecex 8235  ax-cnre 8236
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1737  df-clab 2053  df-cleq 2058  df-clel 2061  df-ne 2185  df-ral 2279  df-rex 2280  df-rab 2282  df-v 2478  df-dif 2797  df-un 2799  df-in 2801  df-ss 2805  df-nul 3074  df-if 3183  df-sn 3262  df-pr 3263  df-op 3265  df-uni 3431  df-br 3593  df-opab 3647  df-xp 4276  df-cnv 4278  df-dm 4280  df-rn 4281  df-res 4282  df-ima 4283  df-fv 4290  df-ov 5369  df-2 9191  df-3 9192  df-4 9193
Copyright terms: Public domain