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 ¬xφ
Assertion nexr ¬φ

Proof

Step Hyp Ref Expression
1 nexr.1 ¬xφ
2 19.8a φxφ
3 1 2 mto ¬φ