Definition df-bnj17 34830

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 34829	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
6	1, 2, 3	w3a 1087	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wa 395	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)
8	5, 7	wb 206	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))

This definition is referenced by:  bnj248  34843  bnj250  34844  bnj258  34851  bnj268  34852  bnj291  34854  bnj312  34855  bnj446  34860  bnj645  34893  bnj658  34894  bnj887  34908  bnj919  34910  bnj945  34916  bnj951  34918  bnj982  34921  bnj1019  34922  bnj518  35028  bnj571  35048  bnj594  35054  bnj916  35075  bnj966  35086  bnj967  35087  bnj1006  35102  bnj1018g  35105  bnj1018  35106  bnj1040  35114  bnj1174  35145  bnj1175  35146  bnj1311  35166