Definition df-bnj17 33388

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

This definition is referenced by:  bnj248  33401  bnj250  33402  bnj258  33409  bnj268  33410  bnj291  33412  bnj312  33413  bnj446  33418  bnj645  33451  bnj658  33452  bnj887  33466  bnj919  33468  bnj945  33474  bnj951  33476  bnj982  33479  bnj1019  33480  bnj518  33587  bnj571  33607  bnj594  33613  bnj916  33634  bnj966  33645  bnj967  33646  bnj1006  33661  bnj1018g  33664  bnj1018  33665  bnj1040  33673  bnj1174  33704  bnj1175  33705  bnj1311  33725