Metamath Proof Explorer


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 ( 𝜑 → ( ∃ 𝑥𝐴𝑦𝐵 𝜓 → ∃ 𝑧𝐶𝑤𝐷 𝜒 ) )