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

Metamath Proof Explorer

Theorem con4d

Description: Deduction associated with con4 . (Contributed by NM, 26-Mar-1995)

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

Step	Hyp	Ref	Expression
1		con4d.1	$⊢ φ \to (\neg ψ \to \neg χ)$
2		con4	$⊢ (\neg ψ \to \neg χ) \to (χ \to ψ)$
3	1 2	syl	$⊢ φ \to (χ \to ψ)$