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

Theorem 2p2e4 8052
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 8020 . . 3
21oveq2i 5041 . 2
3 df-4 8022 . . 3
4 df-3 8021 . . . 4
54oveq1i 5040 . . 3
6 2cn 8030 . . . 4
7 ax-1cn 7312 . . . 4
86, 7, 7addassi 7352 . . 3
93, 5, 83eqtri 1942 . 2
102, 9eqtr4i 1941 1
Colors of variables: wff set class
Syntax hints:   wceq 1414  (class class class)co 5032  c1 7258   caddc 7260  c2 8011  c3 8012  c4 8013
This theorem is referenced by:  2t2e4 8080  i4 9107  ef01bndlem 9949  pythagtriplem1 10236  prmlem2 10469  43prm 10471  1259lem4 10480  2503lem1 10483  2503lem2 10484  2503lem3 10485  4001lem1 10487  4001lem4 10490  quart1lem 14506  log2ub 14598
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-addass 7319  ax-i2m1 7322  ax-1ne0 7323  ax-rrecex 7326  ax-cnre 7327
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-rab 2134  df-v 2329  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-sn 3092  df-pr 3093  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-xp 4048  df-cnv 4050  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fv 4062  df-ov 5034  df-2 8020  df-3 8021  df-4 8022
Copyright terms: Public domain