Theorem axi5r

Description: Converse of axc4 (intuitionistic logic axiom ax-i5r). (Contributed by Jim Kingdon, 31-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		hba1	|- ( A. x ph -> A. x A. x ph )
2		hba1	|- ( A. x ps -> A. x A. x ps )
3	1 2	hbim	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> A. x ps ) )
4		sp	|- ( A. x ps -> ps )
5	4	imim2i	|- ( ( A. x ph -> A. x ps ) -> ( A. x ph -> ps ) )
6	3 5	alrimih	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )