Definition df-4 12303

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

Step	Hyp	Ref	Expression
1		c4 12295	. 2 class 4
2		c3 12294	. . 3 class 3
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12321  4re  12322  4cn  12323  4pos  12345  4m1e3  12367  2p2e4  12373  3p1e4  12383  3p2e5  12389  4p4e8  12393  5p4e9  12396  3lt4  12412  6p4e10  12778  7p4e11  12782  7p7e14  12785  8p4e12  12788  8p6e14  12790  9p4e13  12795  9p5e14  12796  4t4e16  12805  5t4e20  12808  6t4e24  12812  7t4e28  12817  8t4e32  12823  9t4e36  12830  fz0to4untppr  13645  4bc2eq6  14345  bpoly3  16072  bpoly4  16073  fsumcube  16074  ef4p  16129  ef01bndlem  16200  ge2nprmge4  16718  lt6abl  19874  cphipval  25193  sincosq4sgn  26460  binom4  26810  quart1lem  26815  log2cnv  26904  ppiublem2  27164  ppiub  27165  chtub  27173  bclbnd  27241  bposlem8  27252  lgsdir2lem3  27288  3wlkdlem1  30086  ipval2  30634  problem3  35635  aks4d1p1p7  42033  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  lt4addmuld  45283  stoweidlem13  45990  m1modnep2mod  47329  4even  47671  sbgoldbo  47749  ackval40  48621  ackval41a  48622  ackval42  48624