Definition df-bnj17 34664

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 34663	. 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  34677  bnj250  34678  bnj258  34685  bnj268  34686  bnj291  34688  bnj312  34689  bnj446  34694  bnj645  34727  bnj658  34728  bnj887  34742  bnj919  34744  bnj945  34750  bnj951  34752  bnj982  34755  bnj1019  34756  bnj518  34863  bnj571  34883  bnj594  34889  bnj916  34910  bnj966  34921  bnj967  34922  bnj1006  34937  bnj1018g  34940  bnj1018  34941  bnj1040  34949  bnj1174  34980  bnj1175  34981  bnj1311  35001