MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-4 Unicode version

Definition df-4 10374
Description: Define the number 4. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-4

Detailed syntax breakdown of Definition df-4
StepHypRef Expression
1 c4 10365 . 2
2 c3 10364 . . 3
3 c1 9275 . . 3
4 caddc 9277 . . 3
52, 3, 4co 6086 . 2
61, 5wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  4re  10390  4pos  10409  2p2e4  10431  3p1e4  10439  3p2e5  10446  4p4e8  10450  5p4e9  10453  6p4e10  10457  4nn  10473  3lt4  10483  halfpm6th  10538  7p4e11  10799  7p7e14  10802  8p4e12  10804  8p6e14  10806  9p4e13  10811  9p5e14  10812  4t4e16  10820  5t4e20  10822  6t4e24  10826  7t4e28  10831  8t4e32  10837  9t4e36  10844  fzo0to42pr  11608  ef4p  13389  ef01bndlem  13460  lt6abl  16362  iblitg  21226  sincosq4sgn  21943  ang180lem2  22186  binom4  22225  quart1lem  22230  log2cnv  22319  log2ub  22324  ppiublem2  22522  ppiub  22523  chtub  22531  bclbnd  22599  bposlem8  22610  lgsdir2lem3  22644  usgraexvlem  23281  ipval2  24070  problem3  27269  4bc2eq6  27360  bpoly3  28170  bpoly4  28171  fsumcube  28172  rmydioph  29334  rmxdioph  29336  expdiophlem2  29342  stoweidlem13  29779
  Copyright terms: Public domain W3C validator