Definition df-bnj17 33447

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 33446	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 972	. . 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  33460  bnj250  33461  bnj258  33468  bnj268  33469  bnj291  33471  bnj312  33472  bnj446  33477  bnj645  33514  bnj658  33515  bnj887  33530  bnj919  33532  bnj945  33539  bnj951  33541  bnj982  33544  bnj1019  33545  bnj518  33651  bnj571  33671  bnj594  33677  bnj916  33698  bnj966  33709  bnj967  33710  bnj1006  33724  bnj1018  33727  bnj1040  33735  bnj1174  33766  bnj1175  33767  bnj1311  33787