Definition df-bnj17 34985

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

This definition is referenced by:  bnj248  34998  bnj250  34999  bnj258  35006  bnj268  35007  bnj291  35009  bnj312  35010  bnj446  35015  bnj645  35048  bnj658  35049  bnj887  35063  bnj919  35065  bnj945  35071  bnj951  35073  bnj982  35076  bnj1019  35077  bnj518  35183  bnj571  35203  bnj594  35209  bnj916  35230  bnj966  35241  bnj967  35242  bnj1006  35257  bnj1018g  35260  bnj1018  35261  bnj1040  35269  bnj1174  35300  bnj1175  35301  bnj1311  35321