Theorem iscnrm3lem6

Description: Lemma for iscnrm3lem7 . (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypothesis	iscnrm3lem6.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝜓 ) → 𝜒 )
Assertion	iscnrm3lem6	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑊 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3lem6.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝜓 ) → 𝜒 )
2	1	3exp	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) → ( 𝜓 → 𝜒 ) ) )
3	2	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑊 𝜓 → 𝜒 ) )