Metamath Proof Explorer


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 ( ( 𝜑𝜓 ) → 𝜒 )