Metamath Proof Explorer


Theorem hbng

Description: A more general form of hbn . (Contributed by Scott Fenton, 13-Dec-2010)

Ref Expression
Hypothesis hbg.1 φxψ
Assertion hbng ¬ψx¬φ

Proof

Step Hyp Ref Expression
1 hbg.1 φxψ
2 hbntg xφxψ¬ψx¬φ
3 2 1 mpg ¬ψx¬φ