Definition df-bnj17 35021

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

Assertion

Ref	Expression
df-bnj17	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

Detailed syntax breakdown of Definition df-bnj17

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4		wth	. . 3 wff 𝜃
5	1, 2, 3, 4	w-bnj17 35020	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1101	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 400	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  35034  bnj250  35035  bnj258  35042  bnj268  35043  bnj291  35045  bnj312  35046  bnj446  35051  bnj645  35084  bnj658  35085  bnj887  35099  bnj919  35101  bnj945  35107  bnj951  35109  bnj982  35112  bnj1019  35113  bnj518  35219  bnj571  35239  bnj594  35245  bnj916  35266  bnj966  35277  bnj967  35278  bnj1006  35293  bnj1018g  35296  bnj1018  35297  bnj1040  35305  bnj1174  35336  bnj1175  35337  bnj1311  35357