Definition df-bnj17 35227

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 35226	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1103	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 401	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is used by:  bnj248  35240  bnj250  35241  bnj258  35248  bnj268  35249  bnj291  35251  bnj312  35252  bnj446  35257  bnj645  35290  bnj658  35291  bnj887  35305  bnj919  35307  bnj945  35313  bnj951  35315  bnj982  35318  bnj1019  35319  bnj518  35425  bnj571  35445  bnj594  35451  bnj916  35472  bnj966  35483  bnj967  35484  bnj1006  35499  bnj1018g  35502  bnj1018  35503  bnj1040  35511  bnj1174  35542  bnj1175  35543  bnj1311  35563