Metamath Proof Explorer

Theorem sbcthdv

Description: Deduction version of sbcth . (Contributed by NM, 30-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Hypothesis sbcthdv.1 
|- ( ph -> ps )
Assertion sbcthdv 
|- ( ( ph /\ A e. V ) -> [. A / x ]. ps )

Proof

Step Hyp Ref Expression
1 sbcthdv.1 
 |-  ( ph -> ps )
2 1 alrimiv 
 |-  ( ph -> A. x ps )
3 spsbc 
 |-  ( A e. V -> ( A. x ps -> [. A / x ]. ps ) )
4 2 3 mpan9 
 |-  ( ( ph /\ A e. V ) -> [. A / x ]. ps )