Theorem axi5r

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

	Ref	Expression
Assertion	axi5r	⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		hba1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 )
2		hba1	⊢ ( ∀ 𝑥 𝜓 → ∀ 𝑥 ∀ 𝑥 𝜓 )
3	1 2	hbim	⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
4		sp	⊢ ( ∀ 𝑥 𝜓 → 𝜓 )
5	4	imim2i	⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑥 𝜑 → 𝜓 ) )
6	3 5	alrimih	⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) )