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

Metamath Proof Explorer

Theorem expi

Description: An exportation inference. (Contributed by NM, 29-Dec-1992) (Proof shortened by Mel L. O'Cat, 28-Nov-2008)

		Ref	Expression
	Hypothesis	expi.1	$⊢ \neg (φ \to \neg ψ) \to χ$
	Assertion	expi	$⊢ φ \to (ψ \to χ)$

Step	Hyp	Ref	Expression
1		expi.1	$⊢ \neg (φ \to \neg ψ) \to χ$
2		pm3.2im	$⊢ φ \to (ψ \to \neg (φ \to \neg ψ))$
3	2 1	syl6	$⊢ φ \to (ψ \to χ)$