MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2p2e4 Unicode version

Theorem 2p2e4 9889
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/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2p2e4  |-  ( 2  +  2 )  =  4

Proof of Theorem 2p2e4
StepHypRef Expression
1 df-2 9849 . . 3  |-  2  =  ( 1  +  1 )
21oveq2i 5911 . 2  |-  ( 2  +  2 )  =  ( 2  +  ( 1  +  1 ) )
3 df-4 9851 . . 3  |-  4  =  ( 3  +  1 )
4 df-3 9850 . . . 4  |-  3  =  ( 2  +  1 )
54oveq1i 5910 . . 3  |-  ( 3  +  1 )  =  ( ( 2  +  1 )  +  1 )
6 2cn 9861 . . . 4  |-  2  e.  CC
7 ax-1cn 8840 . . . 4  |-  1  e.  CC
86, 7, 7addassi 8890 . . 3  |-  ( ( 2  +  1 )  +  1 )  =  ( 2  +  ( 1  +  1 ) )
93, 5, 83eqtri 2340 . 2  |-  4  =  ( 2  +  ( 1  +  1 ) )
102, 9eqtr4i 2339 1  |-  ( 2  +  2 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1633  (class class class)co 5900   1c1 8783    + caddc 8785   2c2 9840   3c3 9841   4c4 9842
This theorem is referenced by:  2t2e4  9918  i4  11252  ef01bndlem  12511  pythagtriplem1  12916  prmlem2  13168  43prm  13170  1259lem4  13179  2503lem1  13182  2503lem2  13183  2503lem3  13184  4001lem1  13186  4001lem4  13189  quart1lem  20204  log2ub  20298  4bc2eq6  24385  bpoly4  25180  fsumcube  25181  wallispi2lem1  26968  stirlinglem8  26978  2p2ne5  27712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-addass 8847  ax-i2m1 8850  ax-1ne0 8851  ax-rrecex 8854  ax-cnre 8855
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-2 9849  df-3 9850  df-4 9851
  Copyright terms: Public domain W3C validator