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

Theorem 2p2e4 9774
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 9737 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5768 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9739 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9738 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5767 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9749 . . . 4  |-  2  e.  CC
7 ax-1cn 8728 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8778 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2280 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2279 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1619  (class class class)co 5757   1c1 8671    + caddc 8673   2c2 9728   3c3 9729   4c4 9730
This theorem is referenced by:  2t2e4  9803  i4  11136  ef01bndlem  12391  pythagtriplem1  12796  prmlem2  13048  43prm  13050  1259lem4  13059  2503lem1  13062  2503lem2  13063  2503lem3  13064  4001lem1  13066  4001lem4  13069  quart1lem  20078  log2ub  20172  4bc2eq6  23435  bpoly4  24134  fsumcube  24135  2p2ne5  27276
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-resscn 8727  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-addass 8735  ax-i2m1 8738  ax-1ne0 8739  ax-rrecex 8742  ax-cnre 8743
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654  df-ov 5760  df-2 9737  df-3 9738  df-4 9739
  Copyright terms: Public domain W3C validator