Definition df-bnj17 34684

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 34683	. 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  34697  bnj250  34698  bnj258  34705  bnj268  34706  bnj291  34708  bnj312  34709  bnj446  34714  bnj645  34747  bnj658  34748  bnj887  34762  bnj919  34764  bnj945  34770  bnj951  34772  bnj982  34775  bnj1019  34776  bnj518  34883  bnj571  34903  bnj594  34909  bnj916  34930  bnj966  34941  bnj967  34942  bnj1006  34957  bnj1018g  34960  bnj1018  34961  bnj1040  34969  bnj1174  35000  bnj1175  35001  bnj1311  35021