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 ψ