Theorem hbn1 1730

Description: x is not free in ¬ ∀xφ. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)

Assertion

Ref	Expression
hbn1	⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)

Proof of Theorem hbn1

Step	Hyp	Ref	Expression
1		ax-6 1729	1 ⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-6 1729

This theorem is referenced by:  hbe1  1731  modal-5  1733  ax5o  1749  hbnOLD  1777  hba1OLD  1787  hbimdOLD  1816  dvelimhw  1849  ax12olem6  1932  dvelimv  1939  a16g  1945  ax15  2021  dvelimALT  2133  ax11indn  2195