Theorem hbimg

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

	Ref	Expression
Hypotheses	hbg.1	|- ( ph -> A. x ps )
	hbg.2	|- ( ch -> A. x th )
Assertion	hbimg	|- ( ( ps -> ch ) -> A. x ( ph -> th ) )

Proof

Step	Hyp	Ref	Expression
1		hbg.1	|- ( ph -> A. x ps )
2		hbg.2	|- ( ch -> A. x th )
3	1	ax-gen	|- A. x ( ph -> A. x ps )
4		hbimtg	|- ( ( A. x ( ph -> A. x ps ) /\ ( ch -> A. x th ) ) -> ( ( ps -> ch ) -> A. x ( ph -> th ) ) )
5	3 2 4	mp2an	|- ( ( ps -> ch ) -> A. x ( ph -> th ) )