This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spesbcd

Description: form of spsbc . (Contributed by Mario Carneiro, 9-Feb-2017)

Ref Expression
Hypothesis spesbcd.1 
|- ( ph -> [. A / x ]. ps )
Assertion spesbcd 
|- ( ph -> E. x ps )

Proof

Step Hyp Ref Expression
1 spesbcd.1 
 |-  ( ph -> [. A / x ]. ps )
2 spesbc 
 |-  ( [. A / x ]. ps -> E. x ps )
3 1 2 syl 
 |-  ( ph -> E. x ps )