Definition df-rcp-AND5 165

Description: '∧' 5-Tuple.

Assertion

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

Detailed syntax breakdown of Definition df-rcp-AND5

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		wff-ph5	. . 3 wff 𝜑₅
6	1, 2, 3, 4, 5	wff-rcp-AND5 164	. 2 wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅)
7	1, 2, 3, 4	wff-rcp-AND4 162	. . 3 wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄)
8	7, 5	wff-and 132	. 2 wff ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ∧ 𝜑₅)
9	6, 8	wff-bi 104	1 wff ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅) ↔ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ∧ 𝜑₅))

This definition is referenced by:  rcp-NDSEP5  188  rcp-NDJOIN5  191