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

Definition df-4 11694
Description: Define the number 4. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-4 4 = (3 + 1)

Detailed syntax breakdown of Definition df-4
StepHypRef Expression
1 c4 11686 . 2 class 4
2 c3 11685 . . 3 class 3
3 c1 10531 . . 3 class 1
4 caddc 10533 . . 3 class +
52, 3, 4co 7139 . 2 class (3 + 1)
61, 5wceq 1538 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4nn  11712  4re  11713  4cn  11714  4pos  11736  4m1e3  11758  2p2e4  11764  3p1e4  11774  3p2e5  11780  4p4e8  11784  5p4e9  11787  3lt4  11803  halfpm6th  11850  6p4e10  12162  7p4e11  12166  7p7e14  12169  8p4e12  12172  8p6e14  12174  9p4e13  12179  9p5e14  12180  4t4e16  12189  5t4e20  12192  6t4e24  12196  7t4e28  12201  8t4e32  12207  9t4e36  12214  fz0to4untppr  13009  4bc2eq6  13689  bpoly3  15407  bpoly4  15408  fsumcube  15409  ef4p  15461  ef01bndlem  15532  ge2nprmge4  16038  lt6abl  19011  cphipval  23850  sincosq4sgn  25097  binom4  25439  quart1lem  25444  log2cnv  25533  ppiublem2  25790  ppiub  25791  chtub  25799  bclbnd  25867  bposlem8  25878  lgsdir2lem3  25914  3wlkdlem1  27947  ipval2  28493  problem3  33018  rmydioph  39942  rmxdioph  39944  expdiophlem2  39950  lt4addmuld  41925  stoweidlem13  42642  4even  44214  sbgoldbo  44292  ackval40  45094  ackval41a  45095  ackval42  45097
  Copyright terms: Public domain W3C validator