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

Theorem 2p2e4 7791
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 7759 . . 3
21oveq2i 4933 . 2
3 df-4 7761 . . 3
4 df-3 7760 . . . 4
54oveq1i 4932 . . 3
6 2cn 7769 . . . 4
7 ax-1cn 7061 . . . 4
86, 7, 7addassi 7100 . . 3
93, 5, 83eqtri 1953 . 2
102, 9eqtr4i 1952 1
Colors of variables: wff set class
Syntax hints:   wceq 1425  (class class class)co 4924  c1 7007   caddc 7009  c2 7750  c3 7751  c4 7752
This theorem is referenced by:  2t2e4 7811  i4 8730  ef01bndlem 9519  pythagtriplem1 9797  43prm 9985  139prm 9987  163prm 9988  317prm 9989  631prm 9990  1259lem1 9993  1259lem3 9995  1259lem4 9996  1259lem5 9997  2503lem1 9999  2503lem2 10000  2503lem3 10001  4001lem1 10003  4001lem2 10004  4001lem3 10005  4001lem4 10006  bclbnd 12927  bpos1 12930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-addass 7068  ax-i2m1 7071  ax-1ne0 7072  ax-rrecex 7075  ax-cnre 7076
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-v 2337  df-un 2639  df-in 2641  df-ss 2643  df-sn 3080  df-pr 3081  df-op 3083  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4005  df-cnv 4007  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fv 4019  df-ov 4926  df-2 7759  df-3 7760  df-4 7761
Copyright terms: Public domain