Definition df-rcp-AND3 161

Description: '∧' 3-Tuple.

Assertion

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

Detailed syntax breakdown of Definition df-rcp-AND3

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

This definition is referenced by:  rcp-NDSEP3  186  rcp-NDJOIN3  189