Definition df-bnj17 34885

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

This definition is referenced by:  bnj248  34898  bnj250  34899  bnj258  34906  bnj268  34907  bnj291  34909  bnj312  34910  bnj446  34915  bnj645  34948  bnj658  34949  bnj887  34963  bnj919  34965  bnj945  34971  bnj951  34973  bnj982  34976  bnj1019  34977  bnj518  35083  bnj571  35103  bnj594  35109  bnj916  35130  bnj966  35141  bnj967  35142  bnj1006  35157  bnj1018g  35160  bnj1018  35161  bnj1040  35169  bnj1174  35200  bnj1175  35201  bnj1311  35221