Definition df-bnj17 29540

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 29539	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 991	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wa 375	. 2 wff ( ( ph /\ ps /\ ch ) /\ th )
8	5, 7	wb 189	1 wff ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

This definition is referenced by:  bnj248  29553  bnj250  29554  bnj258  29561  bnj268  29562  bnj291  29564  bnj312  29565  bnj446  29570  bnj645  29608  bnj658  29609  bnj887  29624  bnj919  29626  bnj945  29633  bnj951  29635  bnj982  29638  bnj1019  29639  bnj518  29745  bnj571  29765  bnj594  29771  bnj916  29792  bnj966  29803  bnj967  29804  bnj1006  29818  bnj1018  29821  bnj1040  29829  bnj1174  29860  bnj1175  29861  bnj1311  29881