Definition df-bnj17 32675

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

This definition is referenced by:  bnj248  32688  bnj250  32689  bnj258  32696  bnj268  32697  bnj291  32699  bnj312  32700  bnj446  32705  bnj645  32739  bnj658  32740  bnj887  32754  bnj919  32756  bnj945  32762  bnj951  32764  bnj982  32767  bnj1019  32768  bnj518  32875  bnj571  32895  bnj594  32901  bnj916  32922  bnj966  32933  bnj967  32934  bnj1006  32949  bnj1018g  32952  bnj1018  32953  bnj1040  32961  bnj1174  32992  bnj1175  32993  bnj1311  33013