Theorem hbng

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

	Ref	Expression
Hypothesis	hbg.1	|- ( ph -> A. x ps )
Assertion	hbng	|- ( -. ps -> A. x -. ph )

Proof

Step	Hyp	Ref	Expression
1		hbg.1	|- ( ph -> A. x ps )
2		hbntg	|- ( A. x ( ph -> A. x ps ) -> ( -. ps -> A. x -. ph ) )
3	2 1	mpg	|- ( -. ps -> A. x -. ph )