Theorem hbnd

Description: Deduction form of bound-variable hypothesis builder hbn . (Contributed by NM, 3-Jan-2002)

	Ref	Expression
Hypotheses	hbnd.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	hbnd.2	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
Assertion	hbnd	⊢ ( 𝜑 → ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		hbnd.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		hbnd.2	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
3	1 2	alrimih	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) )
4		hbnt	⊢ ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 ) )
5	3 4	syl	⊢ ( 𝜑 → ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 ) )