Definition df-bnj17 31978

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 31977	. 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  31991  bnj250  31992  bnj258  31999  bnj268  32000  bnj291  32002  bnj312  32003  bnj446  32008  bnj645  32045  bnj658  32046  bnj887  32061  bnj919  32063  bnj945  32070  bnj951  32072  bnj982  32075  bnj1019  32076  bnj518  32182  bnj557  32197  bnj571  32202  bnj594  32208  bnj916  32229  bnj966  32240  bnj967  32241  bnj1006  32255  bnj1018  32258  bnj1040  32266  bnj1174  32297  bnj1175  32298  bnj1311  32318