This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exa1

Description: Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion exa1 ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜓 → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )
2 1 eximi ⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜓 → 𝜑 ) )