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ψ