Definition df-bnj17 35085

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

This definition is used by:  bnj248  35098  bnj250  35099  bnj258  35106  bnj268  35107  bnj291  35109  bnj312  35110  bnj446  35115  bnj645  35148  bnj658  35149  bnj887  35163  bnj919  35165  bnj945  35171  bnj951  35173  bnj982  35176  bnj1019  35177  bnj518  35283  bnj571  35303  bnj594  35309  bnj916  35330  bnj966  35341  bnj967  35342  bnj1006  35357  bnj1018g  35360  bnj1018  35361  bnj1040  35369  bnj1174  35400  bnj1175  35401  bnj1311  35421