Definition df-bnj17 34870

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 34869	. 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  34883  bnj250  34884  bnj258  34891  bnj268  34892  bnj291  34894  bnj312  34895  bnj446  34900  bnj645  34933  bnj658  34934  bnj887  34948  bnj919  34950  bnj945  34956  bnj951  34958  bnj982  34961  bnj1019  34962  bnj518  35068  bnj571  35088  bnj594  35094  bnj916  35115  bnj966  35126  bnj967  35127  bnj1006  35142  bnj1018g  35145  bnj1018  35146  bnj1040  35154  bnj1174  35185  bnj1175  35186  bnj1311  35206