Definition df-bnj17 34850

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 34849	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1087	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 395	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 206	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  34863  bnj250  34864  bnj258  34871  bnj268  34872  bnj291  34874  bnj312  34875  bnj446  34880  bnj645  34913  bnj658  34914  bnj887  34928  bnj919  34930  bnj945  34936  bnj951  34938  bnj982  34941  bnj1019  34942  bnj518  35048  bnj571  35068  bnj594  35074  bnj916  35095  bnj966  35106  bnj967  35107  bnj1006  35122  bnj1018g  35125  bnj1018  35126  bnj1040  35134  bnj1174  35165  bnj1175  35166  bnj1311  35186