Metamath Proof Explorer

Theorem nexr

Description: Inference associated with the contrapositive of 19.8a . (Contributed by Jeff Hankins, 26-Jul-2009)

Ref Expression
Hypothesis nexr.1 
|- -. E. x ph
Assertion nexr 
|- -. ph

Proof

Step Hyp Ref Expression
1 nexr.1 
 |-  -. E. x ph
2 19.8a 
 |-  ( ph -> E. x ph )
3 1 2 mto 
 |-  -. ph