Definition df-bnj17 34663

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 34662	. 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  34676  bnj250  34677  bnj258  34684  bnj268  34685  bnj291  34687  bnj312  34688  bnj446  34693  bnj645  34726  bnj658  34727  bnj887  34741  bnj919  34743  bnj945  34749  bnj951  34751  bnj982  34754  bnj1019  34755  bnj518  34862  bnj571  34882  bnj594  34888  bnj916  34909  bnj966  34920  bnj967  34921  bnj1006  34936  bnj1018g  34939  bnj1018  34940  bnj1040  34948  bnj1174  34979  bnj1175  34980  bnj1311  35000