Definition df-bnj17 34677

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 34676	. 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  34690  bnj250  34691  bnj258  34698  bnj268  34699  bnj291  34701  bnj312  34702  bnj446  34707  bnj645  34740  bnj658  34741  bnj887  34755  bnj919  34757  bnj945  34763  bnj951  34765  bnj982  34768  bnj1019  34769  bnj518  34876  bnj571  34896  bnj594  34902  bnj916  34923  bnj966  34934  bnj967  34935  bnj1006  34950  bnj1018g  34953  bnj1018  34954  bnj1040  34962  bnj1174  34993  bnj1175  34994  bnj1311  35014