Definition df-bnj17 35145

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 35144	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1103	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 401	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is used by:  bnj248  35158  bnj250  35159  bnj258  35166  bnj268  35167  bnj291  35169  bnj312  35170  bnj446  35175  bnj645  35208  bnj658  35209  bnj887  35223  bnj919  35225  bnj945  35231  bnj951  35233  bnj982  35236  bnj1019  35237  bnj518  35343  bnj571  35363  bnj594  35369  bnj916  35390  bnj966  35401  bnj967  35402  bnj1006  35417  bnj1018g  35420  bnj1018  35421  bnj1040  35429  bnj1174  35460  bnj1175  35461  bnj1311  35481