Definition df-bnj17 34792

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 34791	. 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  34805  bnj250  34806  bnj258  34813  bnj268  34814  bnj291  34816  bnj312  34817  bnj446  34822  bnj645  34855  bnj658  34856  bnj887  34870  bnj919  34872  bnj945  34878  bnj951  34880  bnj982  34883  bnj1019  34884  bnj518  34991  bnj571  35011  bnj594  35017  bnj916  35038  bnj966  35049  bnj967  35050  bnj1006  35065  bnj1018g  35068  bnj1018  35069  bnj1040  35077  bnj1174  35108  bnj1175  35109  bnj1311  35129