This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hbim1

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

Ref Expression
Hypotheses hbim1.1 ⊢ φ → ∀ x φ
hbim1.2 ⊢ φ → ψ → ∀ x ψ
Assertion hbim1 ⊢ φ → ψ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 hbim1.1 ⊢ φ → ∀ x φ
2 hbim1.2 ⊢ φ → ψ → ∀ x ψ
3 2 a2i ⊢ φ → ψ → φ → ∀ x ψ
4 1 19.21h ⊢ ∀ x φ → ψ ↔ φ → ∀ x ψ
5 3 4 sylibr ⊢ φ → ψ → ∀ x φ → ψ