Definition df-bnj17 32332

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

This definition is referenced by:  bnj248  32345  bnj250  32346  bnj258  32353  bnj268  32354  bnj291  32356  bnj312  32357  bnj446  32362  bnj645  32396  bnj658  32397  bnj887  32411  bnj919  32413  bnj945  32420  bnj951  32422  bnj982  32425  bnj1019  32426  bnj518  32533  bnj571  32553  bnj594  32559  bnj916  32580  bnj966  32591  bnj967  32592  bnj1006  32607  bnj1018g  32610  bnj1018  32611  bnj1040  32619  bnj1174  32650  bnj1175  32651  bnj1311  32671