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

Theorem 2p2e4 7792
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 7760 . . 3 |- 2 = (1 + 1)
21oveq2i 4936 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7762 . . 3 |- 4 = (3 + 1)
4 df-3 7761 . . . 4 |- 3 = (2 + 1)
54oveq1i 4935 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7770 . . . 4 |- 2 e. CC
7 ax-1cn 7062 . . . 4 |- 1 e. CC
86, 7, 7addassi 7101 . . 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 4927  1c1 7008   + caddc 7010  2c2 7751  3c3 7752  4c4 7753
This theorem is referenced by:  2t2e4 7812  i4 8730  ef01bndlem 9517  pythagtriplem1 9795  43prm 9983  139prm 9985  163prm 9986  317prm 9987  631prm 9988  1259lem1 9991  1259lem3 9993  1259lem4 9994  1259lem5 9995  2503lem1 9997  2503lem2 9998  2503lem3 9999  4001lem1 10001  4001lem2 10002  4001lem3 10003  4001lem4 10004  bclbnd 12925  bpos1 12928
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 7061  ax-1cn 7062  ax-icn 7063  ax-addcl 7064  ax-addrcl 7065  ax-mulcl 7066  ax-mulrcl 7067  ax-addass 7069  ax-i2m1 7072  ax-1ne0 7073  ax-rrecex 7076  ax-cnre 7077
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 3085  df-pr 3086  df-op 3088  df-uni 3219  df-br 3364  df-opab 3418  df-xp 4010  df-cnv 4012  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fv 4024  df-ov 4929  df-2 7760  df-3 7761  df-4 7762
Copyright terms: Public domain