Definition df-bnj17 34159

Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bnj17	|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

Detailed syntax breakdown of Definition df-bnj17

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4		wth	. . 3 wff th
5	1, 2, 3, 4	w-bnj17 34158	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 971	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wa 367	. 2 wff ( ( ph /\ ps /\ ch ) /\ th )
8	5, 7	wb 184	1 wff ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

This definition is referenced by:  bnj248  34172  bnj250  34173  bnj258  34180  bnj268  34181  bnj291  34183  bnj312  34184  bnj446  34189  bnj645  34227  bnj658  34228  bnj887  34243  bnj919  34245  bnj945  34252  bnj951  34254  bnj982  34257  bnj1019  34258  bnj518  34364  bnj571  34384  bnj594  34390  bnj916  34411  bnj966  34422  bnj967  34423  bnj1006  34437  bnj1018  34440  bnj1040  34448  bnj1174  34479  bnj1175  34480  bnj1311  34500