Definition df-bnj17 31562

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 31561	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 965	. . 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  31575  bnj250  31576  bnj258  31583  bnj268  31584  bnj291  31586  bnj312  31587  bnj446  31592  bnj645  31629  bnj658  31630  bnj887  31645  bnj919  31647  bnj945  31654  bnj951  31656  bnj982  31659  bnj1019  31660  bnj518  31766  bnj557  31781  bnj571  31786  bnj594  31792  bnj916  31813  bnj966  31824  bnj967  31825  bnj1006  31839  bnj1018  31842  bnj1040  31850  bnj1174  31881  bnj1175  31882  bnj1311  31902