Metamath Proof Explorer


Theorem 19.8ad

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a . (Contributed by DAW, 13-Feb-2017)

Ref Expression
Hypothesis 19.8ad.1 ⊢ φ → ψ
Assertion 19.8ad ⊢ φ → ∃ x ψ

Proof

Step Hyp Ref Expression
1 19.8ad.1 ⊢ φ → ψ
2 19.8a ⊢ ψ → ∃ x ψ
3 1 2 syl ⊢ φ → ∃ x ψ