Definition df-bnj17 34660

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 34659	. 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  34673  bnj250  34674  bnj258  34681  bnj268  34682  bnj291  34684  bnj312  34685  bnj446  34690  bnj645  34723  bnj658  34724  bnj887  34738  bnj919  34740  bnj945  34746  bnj951  34748  bnj982  34751  bnj1019  34752  bnj518  34859  bnj571  34879  bnj594  34885  bnj916  34906  bnj966  34917  bnj967  34918  bnj1006  34933  bnj1018g  34936  bnj1018  34937  bnj1040  34945  bnj1174  34976  bnj1175  34977  bnj1311  34997