Metamath Proof Explorer


Theorem spsbcdi

Description: A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019)

Ref Expression
Hypotheses spsbcdi.1 A V
spsbcdi.2 φ x χ
spsbcdi.3 [˙A / x]˙ χ ψ
Assertion spsbcdi φ ψ

Proof

Step Hyp Ref Expression
1 spsbcdi.1 A V
2 spsbcdi.2 φ x χ
3 spsbcdi.3 [˙A / x]˙ χ ψ
4 1 a1i φ A V
5 4 2 spsbcd φ [˙A / x]˙ χ
6 5 3 sylib φ ψ