Definition df-bnj17 34670

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 34669	. 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  34683  bnj250  34684  bnj258  34691  bnj268  34692  bnj291  34694  bnj312  34695  bnj446  34700  bnj645  34733  bnj658  34734  bnj887  34748  bnj919  34750  bnj945  34756  bnj951  34758  bnj982  34761  bnj1019  34762  bnj518  34869  bnj571  34889  bnj594  34895  bnj916  34916  bnj966  34927  bnj967  34928  bnj1006  34943  bnj1018g  34946  bnj1018  34947  bnj1040  34955  bnj1174  34986  bnj1175  34987  bnj1311  35007