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

Theorem 2p2e4 7955
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 7923 . . 3
21oveq2i 4988 . 2
3 df-4 7925 . . 3
4 df-3 7924 . . . 4
54oveq1i 4987 . . 3
6 2cn 7933 . . . 4
7 ax-1cn 7225 . . . 4
86, 7, 7addassi 7264 . . 3
93, 5, 83eqtri 1942 . 2
102, 9eqtr4i 1941 1
Colors of variables: wff set class
Syntax hints:   wceq 1414  (class class class)co 4979  c1 7171   caddc 7173  c2 7914  c3 7915  c4 7916
This theorem is referenced by:  2t2e4 7975  i4 8900  ef01bndlem 9702  pythagtriplem1 9987  43prm 10178  139prm 10180  163prm 10181  317prm 10182  631prm 10183  1259lem1 10186  1259lem3 10188  1259lem4 10189  1259lem5 10190  2503lem1 10192  2503lem2 10193  2503lem3 10194  4001lem1 10196  4001lem2 10197  4001lem3 10198  4001lem4 10199  bclbnd 13724  bpos1 13727
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 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-addrcl 7228  ax-mulcl 7229  ax-mulrcl 7230  ax-addass 7232  ax-i2m1 7235  ax-1ne0 7236  ax-rrecex 7239  ax-cnre 7240
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-v 2326  df-un 2639  df-in 2641  df-ss 2645  df-sn 3085  df-pr 3086  df-op 3088  df-uni 3224  df-br 3371  df-opab 3425  df-xp 4021  df-cnv 4023  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fv 4035  df-ov 4981  df-2 7923  df-3 7924  df-4 7925
Copyright terms: Public domain