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

Theorem 2p2e4 7769
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 7737 . . 3 |- 2 = (1 + 1)
21oveq2i 4923 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7739 . . 3 |- 4 = (3 + 1)
4 df-3 7738 . . . 4 |- 3 = (2 + 1)
54oveq1i 4922 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7747 . . . 4 |- 2 e. CC
7 ax-1cn 7039 . . . 4 |- 1 e. CC
86, 7, 7addassi 7078 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 1956 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 1955 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1428  (class class class)co 4914  1c1 6985   + caddc 6987  2c2 7728  3c3 7729  4c4 7730
This theorem is referenced by:  2t2e4 7789  i4 8707  ef01bndlem 9494  pythagtriplem1 9770  43prm 9958  139prm 9960  163prm 9961  317prm 9962  631prm 9963  1259lem1 9966  1259lem3 9968  1259lem4 9969  1259lem5 9970  2503lem1 9972  2503lem2 9973  2503lem3 9974  4001lem1 9976  4001lem2 9977  4001lem3 9978  4001lem4 9979  bclbnd 12892  bpos1 12895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914  ax-resscn 7038  ax-1cn 7039  ax-icn 7040  ax-addcl 7041  ax-addrcl 7042  ax-mulcl 7043  ax-mulrcl 7044  ax-addass 7046  ax-i2m1 7049  ax-1ne0 7050  ax-rrecex 7053  ax-cnre 7054
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 917  df-ex 1350  df-sb 1605  df-clab 1920  df-cleq 1925  df-clel 1928  df-ne 2052  df-ral 2145  df-rex 2146  df-v 2339  df-un 2641  df-in 2643  df-ss 2645  df-sn 3077  df-pr 3078  df-op 3080  df-uni 3210  df-br 3355  df-opab 3409  df-xp 4001  df-cnv 4003  df-dm 4005  df-rn 4006  df-res 4007  df-ima 4008  df-fv 4015  df-ov 4916  df-2 7737  df-3 7738  df-4 7739
Copyright terms: Public domain