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

Theorem 2p2e4 7777
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.
Assertion
Ref Expression
2p2e4 |- (2 + 2) = 4

Proof of Theorem 2p2e4
StepHypRef Expression
1 df-2 7745 . . 3 |- 2 = (1 + 1)
21oveq2i 4931 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7747 . . 3 |- 4 = (3 + 1)
4 df-3 7746 . . . 4 |- 3 = (2 + 1)
54oveq1i 4930 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7755 . . . 4 |- 2 e. CC
7 ax-1cn 7047 . . . 4 |- 1 e. CC
86, 7, 7addassi 7086 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 1962 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 1961 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1434  (class class class)co 4922  1c1 6993   + caddc 6995  2c2 7736  3c3 7737  4c4 7738
This theorem is referenced by:  2t2e4 7797  i4 8715  ef01bndlem 9502  pythagtriplem1 9778  43prm 9966  139prm 9968  163prm 9969  317prm 9970  631prm 9971  1259lem1 9974  1259lem3 9976  1259lem4 9977  1259lem5 9978  2503lem1 9980  2503lem2 9981  2503lem3 9982  4001lem1 9984  4001lem2 9985  4001lem3 9986  4001lem4 9987  bclbnd 12903  bpos1 12906
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-resscn 7046  ax-1cn 7047  ax-icn 7048  ax-addcl 7049  ax-addrcl 7050  ax-mulcl 7051  ax-mulrcl 7052  ax-addass 7054  ax-i2m1 7057  ax-1ne0 7058  ax-rrecex 7061  ax-cnre 7062
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3an 923  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-ral 2151  df-rex 2152  df-v 2345  df-un 2647  df-in 2649  df-ss 2651  df-sn 3084  df-pr 3085  df-op 3087  df-uni 3218  df-br 3363  df-opab 3417  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4924  df-2 7745  df-3 7746  df-4 7747
Copyright terms: Public domain