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

Theorem 2p2e4 8703
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

Proof of Theorem 2p2e4
StepHypRef Expression
1 df-2 8671 . . 3
21oveq2i 5215 . 2
3 df-4 8673 . . 3
4 df-3 8672 . . . 4
54oveq1i 5214 . . 3
6 2cn 8681 . . . 4
7 ax-1cn 7963 . . . 4
86, 7, 7addassi 8003 . . 3
93, 5, 83eqtri 2054 . 2
102, 9eqtr4i 2053 1
Colors of variables: wff set class
Syntax hints:   wceq 1526  (class class class)co 5206  c1 7909   caddc 7911  c2 8662  c3 8663  c4 8664
This theorem is referenced by:  2t2e4 8731  i4 9763  ef01bndlem 10610  pythagtriplem1 10900  prmlem2 11133  43prm 11135  1259lem4 11144  2503lem1 11147  2503lem2 11148  2503lem3 11149  4001lem1 11151  4001lem4 11154  quart1lem 15499  log2ub 15593
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-addass 7970  ax-i2m1 7973  ax-1ne0 7974  ax-rrecex 7977  ax-cnre 7978
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-sn 3214  df-pr 3215  df-op 3217  df-uni 3375  df-br 3532  df-opab 3585  df-xp 4186  df-cnv 4188  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fv 4200  df-ov 5208  df-2 8671  df-3 8672  df-4 8673
Copyright terms: Public domain