Definition df-bnj17 29488

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 29487	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 982	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wa 370	. 2 wff ( ( ph /\ ps /\ ch ) /\ th )
8	5, 7	wb 187	1 wff ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

This definition is referenced by:  bnj248  29501  bnj250  29502  bnj258  29509  bnj268  29510  bnj291  29512  bnj312  29513  bnj446  29518  bnj645  29556  bnj658  29557  bnj887  29572  bnj919  29574  bnj945  29581  bnj951  29583  bnj982  29586  bnj1019  29587  bnj518  29693  bnj571  29713  bnj594  29719  bnj916  29740  bnj966  29751  bnj967  29752  bnj1006  29766  bnj1018  29769  bnj1040  29777  bnj1174  29808  bnj1175  29809  bnj1311  29829