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

Metamath Proof Explorer

Theorem spimed

Description: Deduction version of spime . (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 3-Oct-2016) (Proof shortened by Wolf Lammen, 19-Feb-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use spimedv instead. (New usage is discouraged.)

Ref Expression
Hypotheses spimed.1 
|- ( ch -> F/ x ph )
spimed.2 
|- ( x = y -> ( ph -> ps ) )
Assertion spimed 
|- ( ch -> ( ph -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 spimed.1 
 |-  ( ch -> F/ x ph )
2 spimed.2 
 |-  ( x = y -> ( ph -> ps ) )
3 1 nf5rd 
 |-  ( ch -> ( ph -> A. x ph ) )
4 ax6e 
 |-  E. x x = y
5 4 2 eximii 
 |-  E. x ( ph -> ps )
6 5 19.35i 
 |-  ( A. x ph -> E. x ps )
7 3 6 syl6 
 |-  ( ch -> ( ph -> E. x ps ) )