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

Theorem 2p2e4 7999
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 7967 . . 3
21oveq2i 5011 . 2
3 df-4 7969 . . 3
4 df-3 7968 . . . 4
54oveq1i 5010 . . 3
6 2cn 7977 . . . 4
7 ax-1cn 7267 . . . 4
86, 7, 7addassi 7306 . . 3
93, 5, 83eqtri 1942 . 2
102, 9eqtr4i 1941 1
Colors of variables: wff set class
Syntax hints:   wceq 1414  (class class class)co 5002  c1 7213   caddc 7215  c2 7958  c3 7959  c4 7960
This theorem is referenced by:  2t2e4 8019  i4 8966  ef01bndlem 9799  pythagtriplem1 10085  43prm 10277  139prm 10279  163prm 10280  317prm 10281  631prm 10282  1259lem1 10285  1259lem3 10287  1259lem4 10288  1259lem5 10289  2503lem1 10291  2503lem2 10292  2503lem3 10293  4001lem1 10295  4001lem2 10296  4001lem3 10297  4001lem4 10298  bclbnd 14416  bpos1 14419
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 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-addrcl 7270  ax-mulcl 7271  ax-mulrcl 7272  ax-addass 7274  ax-i2m1 7277  ax-1ne0 7278  ax-rrecex 7281  ax-cnre 7282
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 2328  df-un 2641  df-in 2643  df-ss 2647  df-sn 3089  df-pr 3090  df-op 3092  df-uni 3234  df-br 3384  df-opab 3438  df-xp 4035  df-cnv 4037  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fv 4049  df-ov 5004  df-2 7967  df-3 7968  df-4 7969
Copyright terms: Public domain