Definition df-bnj17 35374

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

This definition is used by:  bnj248  35387  bnj250  35388  bnj258  35395  bnj268  35396  bnj291  35398  bnj312  35399  bnj446  35404  bnj645  35437  bnj658  35438  bnj887  35452  bnj919  35454  bnj945  35460  bnj951  35462  bnj982  35465  bnj1019  35466  bnj518  35572  bnj571  35592  bnj594  35598  bnj916  35619  bnj966  35630  bnj967  35631  bnj1006  35646  bnj1018g  35649  bnj1018  35650  bnj1040  35658  bnj1174  35689  bnj1175  35690  bnj1311  35710