Theorem 2p2e4 6138

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	|- (2 + 2) = 4

Proof of Theorem 2p2e4

Step	Hyp	Ref	Expression
1		df-2 6107	. . 3 |- 2 = (1 + 1)
2	1	opreq2i 4025	. 2 |- (2 + 2) = (2 + (1 + 1))
3		df-4 6109	. . 3 |- 4 = (3 + 1)
4		df-3 6108	. . . 4 |- 3 = (2 + 1)
5	4	opreq1i 4024	. . 3 |- (3 + 1) = ((2 + 1) + 1)
6		2cn 6117	. . . 4 |- 2 e. CC
7		ax1cn 5414	. . . 4 |- 1 e. CC
8	6, 7, 7	addassi 5469	. . 3 |- ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 1540	. 2 |- 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 1539	1 |- (2 + 2) = 4

Syntax hints:   = wceq 989  (class class class)co 4016  1c1 5380   + caddc 5382  2c2 6098  3c3 6099  4c4 6100

This theorem is referenced by:  4nn 6139  2t2e4 6159  sqr2gt1lt2 6909  i4 6924  sin01bndlem1 7663  cos01bndlem2 7666  pilem1 8917

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 995  ax-gen 996  ax-8 997  ax-9 998  ax-10 999  ax-11 1000  ax-12 1001  ax-13 1002  ax-14 1003  ax-17 1004  ax-4 1006  ax-5o 1008  ax-6o 1011  ax-9o 1156  ax-10o 1174  ax-16 1244  ax-11o 1252  ax-ext 1498  ax-rep 2763  ax-sep 2773  ax-nul 2780  ax-pow 2813  ax-pr 2851  ax-un 3086  ax-inf2 4761

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1014  df-sb 1206  df-eu 1419  df-mo 1420  df-clab 1504  df-cleq 1509  df-clel 1512  df-ne 1628  df-ral 1693  df-rex 1694  df-reu 1695  df-rab 1696  df-v 1856  df-sbc 1985  df-csb 2050  df-dif 2099  df-un 2100  df-in 2101  df-ss 2103  df-pss 2105  df-nul 2331  df-if 2414  df-pw 2454  df-sn 2465  df-pr 2466  df-tp 2468  df-op 2469  df-uni 2565  df-int 2596  df-iun 2630  df-br 2688  df-opab 2736  df-tr 2750  df-eprel 2906  df-id 2909  df-po 2914  df-so 2926  df-fr 2944  df-we 2959  df-ord 2975  df-on 2976  df-lim 2977  df-suc 2978  df-om 3216  df-xp 3262  df-rel 3263  df-cnv 3264  df-co 3265  df-dm 3266  df-rn 3267  df-res 3268  df-ima 3269  df-fun 3270  df-fn 3271  df-f 3272  df-fv 3276  df-opr 4018  df-oprab 4019  df-1st 4135  df-2nd 4136  df-rdg 4228  df-1o 4264  df-oadd 4266  df-omul 4267  df-er 4396  df-ec 4398  df-qs 4401  df-ni 5145  df-pli 5146  df-mi 5147  df-lti 5148  df-plpq 5180  df-mpq 5181  df-enq 5182  df-nq 5183  df-plq 5184  df-mq 5185  df-rq 5186  df-ltq 5187  df-1q 5188  df-np 5231  df-1p 5232  df-plp 5233  df-mp 5234  df-ltp 5235  df-plpr 5309  df-mpr 5310  df-enr 5311  df-nr 5312  df-plr 5313  df-mr 5314  df-ltr 5315  df-0r 5316  df-1r 5317  df-m1r 5318  df-c 5385  df-0 5386  df-1 5387  df-i 5388  df-r 5389  df-plus 5390  df-mul 5391  df-sub 5501  df-neg 5503  df-2 6107  df-3 6108  df-4 6109

Copyright terms: Public domain