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	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3		wth	⊢ 𝜃
4	0 1 2 3	w-bnj17	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 )
5	0 1 2	w3a	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )
6	5 3	wa	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 )
7	4 6	wb	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )