Metamath Proof Explorer

Theorem exa1

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

Ref Expression
Assertion exa1 
|- ( E. x ph -> E. x ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( ph -> ( ps -> ph ) )
2 1 eximi 
 |-  ( E. x ph -> E. x ( ps -> ph ) )