Theorem hbn

Description: If x is not free in ph , it is not free in -. ph . (Contributed by NM, 10-Jan-1993) (Proof shortened by Wolf Lammen, 17-Dec-2017)

	Ref	Expression
Hypothesis	hbn.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
Assertion	hbn	⊢ ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		hbn.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		hbnt	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
3	2 1	mpg	⊢ ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )