Definition df-bnj17 32819

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 32818	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 973	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wa 369	. 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  32832  bnj250  32833  bnj258  32840  bnj268  32841  bnj291  32843  bnj312  32844  bnj446  32849  bnj645  32886  bnj658  32887  bnj887  32902  bnj919  32904  bnj945  32911  bnj951  32913  bnj982  32916  bnj1019  32917  bnj518  33023  bnj557  33038  bnj571  33043  bnj594  33049  bnj916  33070  bnj966  33081  bnj967  33082  bnj1006  33096  bnj1018  33099  bnj1040  33107  bnj1174  33138  bnj1175  33139  bnj1311  33159