Theorem hbne 699

Description: If x is not free in φ, it is not free in ¬ φ.

Hypothesis

Ref	Expression
hb.1	⊢ (φ → ∀xφ)

Assertion

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

Proof of Theorem hbne

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 ⊢ (φ → ∀xφ)
2	1	con3i 90	. . 3 ⊢ (¬ ∀xφ → ¬ φ)
3	2	19.20i 691	. 2 ⊢ (∀x ¬ ∀xφ → ∀x ¬ φ)
4		ax-6 675	. 2 ⊢ (¬ ∀x ¬ ∀xφ → φ)
5	3, 4	nsyl4 105	1 ⊢ (¬ φ → ∀x ¬ φ)

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672

This theorem is referenced by:  hbex 701  hbim 702  hbor 703  hban 704  hbn1 708  19.32 765  19.41 774  eq6 826  eqsex 834  a4c 843  cbvex 849  sb5y 883  sb8e 919  mo 1020  cla4egf 1395  hbdif 1590

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

metamath.org