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

Theorem 2p2e4 7738
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 7706 . . 3 |- 2 = (1 + 1)
21oveq2i 4933 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7708 . . 3 |- 4 = (3 + 1)
4 df-3 7707 . . . 4 |- 3 = (2 + 1)
54oveq1i 4932 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7716 . . . 4 |- 2 e. CC
7 ax-1cn 7015 . . . 4 |- 1 e. CC
86, 7, 7addassi 7054 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 1984 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 1983 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1457  (class class class)co 4924  1c1 6961   + caddc 6963  2c2 7697  3c3 7698  4c4 7699
This theorem is referenced by:  2t2e4 7758  i4 8661  sqr2gt1lt2 8945  ef01bndlem 9404  pythagtriplem1 9676  43prm 9816  139prm 9818  163prm 9819  317prm 9820  631prm 9821  1259lem1 9824  1259lem3 9826  1259lem4 9827  1259lem5 9828  2503lem1 9830  2503lem2 9831  2503lem3 9832  4001lem1 9834  4001lem2 9835  4001lem3 9836  4001lem4 9837  bclbnd 11931  bpos1 11939
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 1671  ax-ext 1942  ax-resscn 7014  ax-1cn 7015  ax-icn 7016  ax-addcl 7017  ax-addrcl 7018  ax-mulcl 7019  ax-mulrcl 7020  ax-addass 7022  ax-i2m1 7025  ax-1ne0 7026  ax-rrecex 7029  ax-cnre 7030
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-v 2367  df-un 2667  df-in 2669  df-ss 2671  df-sn 3099  df-pr 3100  df-op 3103  df-uni 3232  df-br 3377  df-opab 3431  df-xp 4014  df-cnv 4016  df-dm 4018  df-rn 4019  df-res 4020  df-ima 4021  df-fv 4028  df-ov 4926  df-2 7706  df-3 7707  df-4 7708
Copyright terms: Public domain