Theorem hbim1

Description: A closed form of hbim . (Contributed by NM, 2-Jun-1993)

	Ref	Expression
Hypotheses	hbim1.1	|- ( ph -> A. x ph )
	hbim1.2	|- ( ph -> ( ps -> A. x ps ) )
Assertion	hbim1	|- ( ( ph -> ps ) -> A. x ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		hbim1.1	|- ( ph -> A. x ph )
2		hbim1.2	|- ( ph -> ( ps -> A. x ps ) )
3	2	a2i	|- ( ( ph -> ps ) -> ( ph -> A. x ps ) )
4	1	19.21h	|- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
5	3 4	sylibr	|- ( ( ph -> ps ) -> A. x ( ph -> ps ) )