Theorem bj-nexdh2

Description: Uncurried (imported) form of bj-nexdh . (Contributed by BJ, 6-May-2019)

	Ref	Expression
Assertion	bj-nexdh2	⊢ ( ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ( 𝜒 → ∀ 𝑥 𝜑 ) ) → ( 𝜒 → ¬ ∃ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nexdh	⊢ ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) → ( ( 𝜒 → ∀ 𝑥 𝜑 ) → ( 𝜒 → ¬ ∃ 𝑥 𝜓 ) ) )
2	1	imp	⊢ ( ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ( 𝜒 → ∀ 𝑥 𝜑 ) ) → ( 𝜒 → ¬ ∃ 𝑥 𝜓 ) )