Theorem reximddv2

Description: Double deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	reximddv2.1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
	reximddv2.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion	reximddv2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		reximddv2.1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
2		reximddv2.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
3	1	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜓 → 𝜒 ) )
4	3	reximdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑦 ∈ 𝐵 𝜒 ) )
5	4	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) → ∃ 𝑦 ∈ 𝐵 𝜒 )
6	5 2	reximddv	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 )