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 4940 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7752 . . 3 |- 4 = (3 + 1)
4 df-3 7751 . . . 4 |- 3 = (2 + 1)
54oveq1i 4939 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7760 . . . 4 |- 2 e. CC
7 ax-1cn 7053 . . . 4 |- 1 e. CC
86, 7, 7addassi 7092 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 1977 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 1976 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1449  (class class class)co 4931  1c1 6999   + caddc 7001  2c2 7741  3c3 7742  4c4 7743
This theorem is referenced by:  2t2e4 7802  i4 8716  sqr2gt1lt2 9000  ef01bndlem 9451  pythagtriplem1 9726  43prm 9880  139prm 9882  163prm 9883  317prm 9884  631prm 9885  1259lem1 9888  1259lem3 9890  1259lem4 9891  1259lem5 9892  2503lem1 9894  2503lem2 9895  2503lem3 9896  4001lem1 9898  4001lem2 9899  4001lem3 9900  4001lem4 9901  bclbnd 12709  bpos1 12717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-resscn 7052  ax-1cn 7053  ax-icn 7054  ax-addcl 7055  ax-addrcl 7056  ax-mulcl 7057  ax-mulrcl 7058  ax-addass 7060  ax-i2m1 7063  ax-1ne0 7064  ax-rrecex 7067  ax-cnre 7068
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3an 939  df-ex 1372  df-sb 1626  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-ral 2166  df-rex 2167  df-v 2360  df-un 2662  df-in 2664  df-ss 2666  df-sn 3096  df-pr 3097  df-op 3100  df-uni 3229  df-br 3374  df-opab 3428  df-xp 4018  df-cnv 4020  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fv 4032  df-ov 4933  df-2 7750  df-3 7751  df-4 7752
Copyright terms: Public domain