Metamath Proof Explorer

Theorem axi5r

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

Ref Expression
Assertion axi5r ⊢ ∀ x φ → ∀ x ψ → ∀ x ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 hba1 ⊢ ∀ x φ → ∀ x ∀ x φ
2 hba1 ⊢ ∀ x ψ → ∀ x ∀ x ψ
3 1 2 hbim ⊢ ∀ x φ → ∀ x ψ → ∀ x ∀ x φ → ∀ x ψ
4 sp ⊢ ∀ x ψ → ψ
5 4 imim2i ⊢ ∀ x φ → ∀ x ψ → ∀ x φ → ψ
6 3 5 alrimih ⊢ ∀ x φ → ∀ x ψ → ∀ x ∀ x φ → ψ