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

Theorem 2p2e4 7892
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 7860 . . 3
21oveq2i 4953 . 2
3 df-4 7862 . . 3
4 df-3 7861 . . . 4
54oveq1i 4952 . . 3
6 2cn 7870 . . . 4
7 ax-1cn 7162 . . . 4
86, 7, 7addassi 7201 . . 3
93, 5, 83eqtri 1941 . 2
102, 9eqtr4i 1940 1
Colors of variables: wff set class
Syntax hints:   wceq 1413  (class class class)co 4944  c1 7108   caddc 7110  c2 7851  c3 7852  c4 7853
This theorem is referenced by:  2t2e4 7912  i4 8834  ef01bndlem 9636  pythagtriplem1 9920  43prm 10111  139prm 10113  163prm 10114  317prm 10115  631prm 10116  1259lem1 10119  1259lem3 10121  1259lem4 10122  1259lem5 10123  2503lem1 10125  2503lem2 10126  2503lem3 10127  4001lem1 10129  4001lem2 10130  4001lem3 10131  4001lem4 10132  bclbnd 13534  bpos1 13537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-addass 7169  ax-i2m1 7172  ax-1ne0 7173  ax-rrecex 7176  ax-cnre 7177
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-v 2324  df-un 2637  df-in 2639  df-ss 2641  df-sn 3079  df-pr 3080  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4946  df-2 7860  df-3 7861  df-4 7862
Copyright terms: Public domain