Theorem iscnrm3lem7

Description: Lemma for iscnrm3rlem8 and iscnrm3llem2 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3lem7.1	⊢ ( 𝑧 = 𝑍 → ( 𝜒 ↔ 𝜃 ) )
	iscnrm3lem7.2	⊢ ( 𝑤 = 𝑊 → ( 𝜃 ↔ 𝜏 ) )
	iscnrm3lem7.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) )
Assertion	iscnrm3lem7	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3lem7.1	⊢ ( 𝑧 = 𝑍 → ( 𝜒 ↔ 𝜃 ) )
2		iscnrm3lem7.2	⊢ ( 𝑤 = 𝑊 → ( 𝜃 ↔ 𝜏 ) )
3		iscnrm3lem7.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) )
4	1 2	rspc2ev	⊢ ( ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 )
5	3 4	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 )
6	5	iscnrm3lem6	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) )