Theorem exlimddvf

Description: A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019)

	Ref	Expression
Hypotheses	exlimddvf.1	⊢ ( 𝜑 → ∃ 𝑥 𝜃 )
	exlimddvf.2	⊢ Ⅎ 𝑥 𝜓
	exlimddvf.3	⊢ ( ( 𝜃 ∧ 𝜓 ) → 𝜒 )
	exlimddvf.4	⊢ Ⅎ 𝑥 𝜒
Assertion	exlimddvf	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		exlimddvf.1	⊢ ( 𝜑 → ∃ 𝑥 𝜃 )
2		exlimddvf.2	⊢ Ⅎ 𝑥 𝜓
3		exlimddvf.3	⊢ ( ( 𝜃 ∧ 𝜓 ) → 𝜒 )
4		exlimddvf.4	⊢ Ⅎ 𝑥 𝜒
5	3	expcom	⊢ ( 𝜓 → ( 𝜃 → 𝜒 ) )
6	2 4 5	exlimd	⊢ ( 𝜓 → ( ∃ 𝑥 𝜃 → 𝜒 ) )
7	1 6	mpan9	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )