Definition df-bnj17 34701

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 34700	. 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  34714  bnj250  34715  bnj258  34722  bnj268  34723  bnj291  34725  bnj312  34726  bnj446  34731  bnj645  34764  bnj658  34765  bnj887  34779  bnj919  34781  bnj945  34787  bnj951  34789  bnj982  34792  bnj1019  34793  bnj518  34900  bnj571  34920  bnj594  34926  bnj916  34947  bnj966  34958  bnj967  34959  bnj1006  34974  bnj1018g  34977  bnj1018  34978  bnj1040  34986  bnj1174  35017  bnj1175  35018  bnj1311  35038