Definition df-bnj17 32566

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

This definition is referenced by:  bnj248  32579  bnj250  32580  bnj258  32587  bnj268  32588  bnj291  32590  bnj312  32591  bnj446  32596  bnj645  32630  bnj658  32631  bnj887  32645  bnj919  32647  bnj945  32653  bnj951  32655  bnj982  32658  bnj1019  32659  bnj518  32766  bnj571  32786  bnj594  32792  bnj916  32813  bnj966  32824  bnj967  32825  bnj1006  32840  bnj1018g  32843  bnj1018  32844  bnj1040  32852  bnj1174  32883  bnj1175  32884  bnj1311  32904