Definition df-bnj17 34879

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 34878	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1092	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 396	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 207	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  34892  bnj250  34893  bnj258  34900  bnj268  34901  bnj291  34903  bnj312  34904  bnj446  34909  bnj645  34942  bnj658  34943  bnj887  34957  bnj919  34959  bnj945  34965  bnj951  34967  bnj982  34970  bnj1019  34971  bnj518  35077  bnj571  35097  bnj594  35103  bnj916  35124  bnj966  35135  bnj967  35136  bnj1006  35151  bnj1018g  35154  bnj1018  35155  bnj1040  35163  bnj1174  35194  bnj1175  35195  bnj1311  35215