Definition df-bnj17 31950

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 31949	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1082	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 398	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 208	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  31963  bnj250  31964  bnj258  31971  bnj268  31972  bnj291  31974  bnj312  31975  bnj446  31980  bnj645  32014  bnj658  32015  bnj887  32029  bnj919  32031  bnj945  32038  bnj951  32040  bnj982  32043  bnj1019  32044  bnj518  32151  bnj571  32171  bnj594  32177  bnj916  32198  bnj966  32209  bnj967  32210  bnj1006  32225  bnj1018g  32228  bnj1018  32229  bnj1040  32237  bnj1174  32268  bnj1175  32269  bnj1311  32289