Definition df-bnj17 34845

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

This definition is referenced by:  bnj248  34858  bnj250  34859  bnj258  34866  bnj268  34867  bnj291  34869  bnj312  34870  bnj446  34875  bnj645  34908  bnj658  34909  bnj887  34923  bnj919  34925  bnj945  34931  bnj951  34933  bnj982  34936  bnj1019  34937  bnj518  35044  bnj571  35064  bnj594  35070  bnj916  35091  bnj966  35102  bnj967  35103  bnj1006  35118  bnj1018g  35121  bnj1018  35122  bnj1040  35130  bnj1174  35161  bnj1175  35162  bnj1311  35182