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

Metamath Proof Explorer

Theorem hbnt

Description: Closed theorem version of bound-variable hypothesis builder hbn . (Contributed by NM, 10-May-1993) (Proof shortened by Wolf Lammen, 14-Oct-2021)

Ref Expression
Assertion hbnt ⊢ ∀ x φ → ∀ x φ → ¬ φ → ∀ x ¬ φ

Proof

Step Hyp Ref Expression
1 nf5-1 ⊢ ∀ x φ → ∀ x φ → Ⅎ x φ
2 1 nfnd ⊢ ∀ x φ → ∀ x φ → Ⅎ x ¬ φ
3 2 nf5rd ⊢ ∀ x φ → ∀ x φ → ¬ φ → ∀ x ¬ φ