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

Metamath Proof Explorer

Theorem hbntg

Description: A more general form of hbnt . (Contributed by Scott Fenton, 13-Dec-2010)

Ref Expression
Assertion hbntg ⊢ ∀ x φ → ∀ x ψ → ¬ ψ → ∀ x ¬ φ

Proof

Step Hyp Ref Expression
1 axc7 ⊢ ¬ ∀ x ¬ ∀ x ψ → ψ
2 1 con1i ⊢ ¬ ψ → ∀ x ¬ ∀ x ψ
3 con3 ⊢ φ → ∀ x ψ → ¬ ∀ x ψ → ¬ φ
4 3 al2imi ⊢ ∀ x φ → ∀ x ψ → ∀ x ¬ ∀ x ψ → ∀ x ¬ φ
5 2 4 syl5 ⊢ ∀ x φ → ∀ x ψ → ¬ ψ → ∀ x ¬ φ