Theorem hbntg

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

	Ref	Expression
Assertion	hbntg	|- ( A. x ( ph -> A. x ps ) -> ( -. ps -> A. x -. ph ) )

Proof

Step	Hyp	Ref	Expression
1		axc7	|- ( -. A. x -. A. x ps -> ps )
2	1	con1i	|- ( -. ps -> A. x -. A. x ps )
3		con3	|- ( ( ph -> A. x ps ) -> ( -. A. x ps -> -. ph ) )
4	3	al2imi	|- ( A. x ( ph -> A. x ps ) -> ( A. x -. A. x ps -> A. x -. ph ) )
5	2 4	syl5	|- ( A. x ( ph -> A. x ps ) -> ( -. ps -> A. x -. ph ) )