Definition df-bnj17 34679

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 34678	. 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  34692  bnj250  34693  bnj258  34700  bnj268  34701  bnj291  34703  bnj312  34704  bnj446  34709  bnj645  34742  bnj658  34743  bnj887  34757  bnj919  34759  bnj945  34765  bnj951  34767  bnj982  34770  bnj1019  34771  bnj518  34878  bnj571  34898  bnj594  34904  bnj916  34925  bnj966  34936  bnj967  34937  bnj1006  34952  bnj1018g  34955  bnj1018  34956  bnj1040  34964  bnj1174  34995  bnj1175  34996  bnj1311  35016