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

Metamath Proof Explorer

Theorem hbnd

Description: Deduction form of bound-variable hypothesis builder hbn . (Contributed by NM, 3-Jan-2002)

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

Proof

Step Hyp Ref Expression
1 hbnd.1 ⊢ φ → ∀ x φ
2 hbnd.2 ⊢ φ → ψ → ∀ x ψ
3 1 2 alrimih ⊢ φ → ∀ x ψ → ∀ x ψ
4 hbnt ⊢ ∀ x ψ → ∀ x ψ → ¬ ψ → ∀ x ¬ ψ
5 3 4 syl ⊢ φ → ¬ ψ → ∀ x ¬ ψ