Definition df-bnj17 34189

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

This definition is referenced by:  bnj248  34202  bnj250  34203  bnj258  34210  bnj268  34211  bnj291  34213  bnj312  34214  bnj446  34219  bnj645  34252  bnj658  34253  bnj887  34267  bnj919  34269  bnj945  34275  bnj951  34277  bnj982  34280  bnj1019  34281  bnj518  34388  bnj571  34408  bnj594  34414  bnj916  34435  bnj966  34446  bnj967  34447  bnj1006  34462  bnj1018g  34465  bnj1018  34466  bnj1040  34474  bnj1174  34505  bnj1175  34506  bnj1311  34526