Definition df-bnj17 33767

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

This definition is referenced by:  bnj248  33780  bnj250  33781  bnj258  33788  bnj268  33789  bnj291  33791  bnj312  33792  bnj446  33797  bnj645  33830  bnj658  33831  bnj887  33845  bnj919  33847  bnj945  33853  bnj951  33855  bnj982  33858  bnj1019  33859  bnj518  33966  bnj571  33986  bnj594  33992  bnj916  34013  bnj966  34024  bnj967  34025  bnj1006  34040  bnj1018g  34043  bnj1018  34044  bnj1040  34052  bnj1174  34083  bnj1175  34084  bnj1311  34104