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

Theorem 2p2e4 7782
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 7750 . . 3 |- 2 = (1 + 1)
21oveq2i 4944 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7752 . . 3 |- 4 = (3 + 1)
4 df-3 7751 . . . 4 |- 3 = (2 + 1)
54oveq1i 4943 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7760 . . . 4 |- 2 e. CC
7 ax-1cn 7054 . . . 4 |- 1 e. CC
86, 7, 7addassi 7093 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 1985 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 1984 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1457  (class class class)co 4935  1c1 7000   + caddc 7002  2c2 7741  3c3 7742  4c4 7743
This theorem is referenced by:  2t2e4 7802  i4 8713  sqr2gt1lt2 8999  ef01bndlem 9435  pythagtriplem1 9710  43prm 9858  139prm 9860  163prm 9861  317prm 9862  631prm 9863  1259lem1 9866  1259lem3 9868  1259lem4 9869  1259lem5 9870  2503lem1 9872  2503lem2 9873  2503lem3 9874  4001lem1 9876  4001lem2 9877  4001lem3 9878  4001lem4 9879  bclbnd 12541  bpos1 12549
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1672  ax-ext 1943  ax-resscn 7053  ax-1cn 7054  ax-icn 7055  ax-addcl 7056  ax-addrcl 7057  ax-mulcl 7058  ax-mulrcl 7059  ax-addass 7061  ax-i2m1 7064  ax-1ne0 7065  ax-rrecex 7068  ax-cnre 7069
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1634  df-clab 1949  df-cleq 1954  df-clel 1957  df-ne 2081  df-ral 2174  df-rex 2175  df-v 2368  df-un 2668  df-in 2670  df-ss 2672  df-sn 3102  df-pr 3103  df-op 3106  df-uni 3235  df-br 3380  df-opab 3434  df-xp 4022  df-cnv 4024  df-dm 4026  df-rn 4027  df-res 4028  df-ima 4029  df-fv 4036  df-ov 4937  df-2 7750  df-3 7751  df-4 7752
Copyright terms: Public domain