Definition df-bnj17 35318

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 35317	. 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  35331  bnj250  35332  bnj258  35339  bnj268  35340  bnj291  35342  bnj312  35343  bnj446  35348  bnj645  35381  bnj658  35382  bnj887  35396  bnj919  35398  bnj945  35404  bnj951  35406  bnj982  35409  bnj1019  35410  bnj518  35516  bnj571  35536  bnj594  35542  bnj916  35563  bnj966  35574  bnj967  35575  bnj1006  35590  bnj1018g  35593  bnj1018  35594  bnj1040  35602  bnj1174  35633  bnj1175  35634  bnj1311  35654