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

Theorem 2p2e4 9661
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 9624 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5696 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9626 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9625 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5695 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9636 . . . 4  |-  2  e.  CC
7 ax-1cn 8649 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8699 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2265 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2264 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1608  (class class class)co 5685   1c1 8592    + caddc 8594   2c2 9615   3c3 9616   4c4 9617
This theorem is referenced by:  2t2e4  9690  i4  11019  ef01bndlem  12272  pythagtriplem1  12677  prmlem2  12929  43prm  12931  1259lem4  12940  2503lem1  12943  2503lem2  12944  2503lem3  12945  4001lem1  12947  4001lem4  12950  quart1lem  19801  log2ub  19895  4bc2eq6  23072  bpoly4  23774  fsumcube  23775
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-resscn 8648  ax-1cn 8649  ax-icn 8650  ax-addcl 8651  ax-addrcl 8652  ax-mulcl 8653  ax-mulrcl 8654  ax-addass 8656  ax-i2m1 8659  ax-1ne0 8660  ax-rrecex 8663  ax-cnre 8664
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-3an 935  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-ne 2402  df-ral 2499  df-rex 2500  df-rab 2502  df-v 2714  df-dif 3061  df-un 3063  df-in 3065  df-ss 3069  df-nul 3343  df-if 3451  df-sn 3530  df-pr 3531  df-op 3533  df-uni 3708  df-br 3901  df-opab 3955  df-xp 4573  df-cnv 4575  df-dm 4577  df-rn 4578  df-res 4579  df-ima 4580  df-fv 4587  df-ov 5688  df-2 9624  df-3 9625  df-4 9626
  Copyright terms: Public domain W3C validator