Definition df-bnj17

Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bnj17	|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3		wth	|- th
4	0 1 2 3	w-bnj17	|- ( ph /\ ps /\ ch /\ th )
5	0 1 2	w3a	|- ( ph /\ ps /\ ch )
6	5 3	wa	|- ( ( ph /\ ps /\ ch ) /\ th )
7	4 6	wb	|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )