Definition df-rcp-AND4 163

Description: '∧' 4-Tuple.

Assertion

Ref	Expression
df-rcp-AND4	⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ↔ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃) ∧ 𝜑₄))

Detailed syntax breakdown of Definition df-rcp-AND4

Step	Hyp	Ref	Expression
1		wff-ph1	. . 3 wff 𝜑₁
2		wff-ph2	. . 3 wff 𝜑₂
3		wff-ph3	. . 3 wff 𝜑₃
4		wff-ph4	. . 3 wff 𝜑₄
5	1, 2, 3, 4	wff-rcp-AND4 162	. 2 wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄)
6	1, 2, 3	wff-rcp-AND3 160	. . 3 wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃)
7	6, 4	wff-and 132	. 2 wff ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃) ∧ 𝜑₄)
8	5, 7	wff-bi 104	1 wff ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ↔ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃) ∧ 𝜑₄))

This definition is referenced by:  rcp-NDSEP4  187  rcp-NDJOIN4  190