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

Theorem 2p2e4 8861
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 8829 . . 3
21oveq2i 5305 . 2
3 df-4 8831 . . 3
4 df-3 8830 . . . 4
54oveq1i 5304 . . 3
6 2cn 8839 . . . 4
7 ax-1cn 8118 . . . 4
86, 7, 7addassi 8160 . . 3
93, 5, 83eqtri 2114 . 2
102, 9eqtr4i 2113 1
Colors of variables: wff set class
Syntax hints:   wceq 1531  (class class class)co 5296  c1 8062   caddc 8064  c2 8820  c3 8821  c4 8822
This theorem is referenced by:  2t2e4  8889  i4  9926  ef01bndlem  10775  pythagtriplem1  11068  prmlem2  11318  43prm  11320  1259lem4  11329  2503lem1  11332  2503lem2  11333  2503lem3  11334  4001lem1  11336  4001lem4  11339  quart1lem  15772  log2ub  15866
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-addass 8125  ax-i2m1 8128  ax-1ne0 8129  ax-rrecex 8132  ax-cnre 8133
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-xp 4263  df-cnv 4265  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fv 4277  df-ov 5298  df-2 8829  df-3 8830  df-4 8831
Copyright terms: Public domain