Definition df-bnj17 34254

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

This definition is referenced by:  bnj248  34267  bnj250  34268  bnj258  34275  bnj268  34276  bnj291  34278  bnj312  34279  bnj446  34284  bnj645  34317  bnj658  34318  bnj887  34332  bnj919  34334  bnj945  34340  bnj951  34342  bnj982  34345  bnj1019  34346  bnj518  34453  bnj571  34473  bnj594  34479  bnj916  34500  bnj966  34511  bnj967  34512  bnj1006  34527  bnj1018g  34530  bnj1018  34531  bnj1040  34539  bnj1174  34570  bnj1175  34571  bnj1311  34591