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

Theorem 2p2e4 9689
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 9652 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5718 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9654 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9653 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5717 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9664 . . . 4  |-  2  e.  CC
7 ax-1cn 8672 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8722 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2277 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2276 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1619  (class class class)co 5707   1c1 8615    + caddc 8617   2c2 9643   3c3 9644   4c4 9645
This theorem is referenced by:  2t2e4  9718  i4  11047  ef01bndlem  12300  pythagtriplem1  12705  prmlem2  12957  43prm  12959  1259lem4  12968  2503lem1  12971  2503lem2  12972  2503lem3  12973  4001lem1  12975  4001lem4  12978  quart1lem  19917  log2ub  20011  4bc2eq6  23198  bpoly4  23897  fsumcube  23898  2p2ne5  26891
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 1926  ax-ext 2234  ax-resscn 8671  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-addrcl 8675  ax-mulcl 8676  ax-mulrcl 8677  ax-addass 8679  ax-i2m1 8682  ax-1ne0 8683  ax-rrecex 8686  ax-cnre 8687
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-xp 4591  df-cnv 4593  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fv 4605  df-ov 5710  df-2 9652  df-3 9653  df-4 9654
  Copyright terms: Public domain W3C validator