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

Theorem 2p2e4 7847
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 7816 . . 3 |- 2 = (1 + 1)
21opreq2i 5076 . 2 |- (2 + 2) = (2 + (1 + 1))
3 df-4 7818 . . 3 |- 4 = (3 + 1)
4 df-3 7817 . . . 4 |- 3 = (2 + 1)
54opreq1i 5075 . . 3 |- (3 + 1) = ((2 + 1) + 1)
6 2cn 7826 . . . 4 |- 2 e. CC
7 ax-1cn 7161 . . . 4 |- 1 e. CC
86, 7, 7addassi 7200 . . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 2116 . 2 |- 4 = (2 + (1 + 1))
102, 9eqtr4i 2115 1 |- (2 + 2) = 4
Colors of variables: wff set class
Syntax hints:   = wceq 1592  (class class class)co 5067  1c1 7107   + caddc 7109  2c2 7807  3c3 7808  4c4 7809
This theorem is referenced by:  2t2e4 7867  i4 8798  sqr2gt1lt2 8974  sin01bndlem1 9679  cos01bndlem2 9682  pilem1 11546  43prm 13744  139prm 13746  163prm 13747  317prm 13748  631prm 13749  1259lem1 13752  1259lem3 13754  1259lem4 13755  1259lem5 13756  2503lem1 13758  2503lem2 13759  2503lem3 13760  4001lem1 13762  4001lem2 13763  4001lem3 13764  4001lem4 13765  bclbnd2 13774  bpos1 13782  pcoass 16720
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609  ax-nul 3619  ax-pr 3679  ax-resscn 7160  ax-1cn 7161  ax-icn 7162  ax-addcl 7163  ax-addrcl 7164  ax-mulcl 7165  ax-mulrcl 7166  ax-addass 7168  ax-i2m1 7171  ax-1ne0 7172  ax-rrecex 7175  ax-cnre 7176
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-sn 3237  df-pr 3238  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-xp 4151  df-cnv 4153  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fv 4165  df-opr 5069  df-2 7816  df-3 7817  df-4 7818
Copyright terms: Public domain