Theorem axi5r

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

	Ref	Expression
Assertion	axi5r	$$⊢\left(\forall x\phi \to \forall x\psi \right)\to \forall x\left(\forall x\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		hba1	$$⊢\forall x\phi \to \forall x\forall x\phi$$
2		hba1	$$⊢\forall x\psi \to \forall x\forall x\psi$$
3	1 2	hbim	$$⊢\left(\forall x\phi \to \forall x\psi \right)\to \forall x\left(\forall x\phi \to \forall x\psi \right)$$
4		sp	$$⊢\forall x\psi \to \psi$$
5	4	imim2i	$$⊢\left(\forall x\phi \to \forall x\psi \right)\to \left(\forall x\phi \to \psi \right)$$
6	3 5	alrimih	$$⊢\left(\forall x\phi \to \forall x\psi \right)\to \forall x\left(\forall x\phi \to \psi \right)$$