This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-nexdh2

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

		Ref	Expression
	Assertion	bj-nexdh2	$⊢ (\forall x (φ \to \neg ψ) \land (χ \to \forall x φ)) \to (χ \to \neg \exists x ψ)$

Step	Hyp	Ref	Expression
1		bj-nexdh	$⊢ \forall x (φ \to \neg ψ) \to ((χ \to \forall x φ) \to (χ \to \neg \exists x ψ))$
2	1	imp	$⊢ (\forall x (φ \to \neg ψ) \land (χ \to \forall x φ)) \to (χ \to \neg \exists x ψ)$