Definition df-bnj17 34699

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

This definition is referenced by:  bnj248  34712  bnj250  34713  bnj258  34720  bnj268  34721  bnj291  34723  bnj312  34724  bnj446  34729  bnj645  34762  bnj658  34763  bnj887  34777  bnj919  34779  bnj945  34785  bnj951  34787  bnj982  34790  bnj1019  34791  bnj518  34898  bnj571  34918  bnj594  34924  bnj916  34945  bnj966  34956  bnj967  34957  bnj1006  34972  bnj1018g  34975  bnj1018  34976  bnj1040  34984  bnj1174  35015  bnj1175  35016  bnj1311  35036