Definition df-bnj17 33698

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 33697	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1088	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 397	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 205	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  33711  bnj250  33712  bnj258  33719  bnj268  33720  bnj291  33722  bnj312  33723  bnj446  33728  bnj645  33761  bnj658  33762  bnj887  33776  bnj919  33778  bnj945  33784  bnj951  33786  bnj982  33789  bnj1019  33790  bnj518  33897  bnj571  33917  bnj594  33923  bnj916  33944  bnj966  33955  bnj967  33956  bnj1006  33971  bnj1018g  33974  bnj1018  33975  bnj1040  33983  bnj1174  34014  bnj1175  34015  bnj1311  34035