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

Metamath Proof Explorer

Theorem 3imp31

Description: The importation inference 3imp with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016)

		Ref	Expression
	Hypothesis	3imp.1	$⊢ φ \to (ψ \to (χ \to θ))$
	Assertion	3imp31	$⊢ (χ \land ψ \land φ) \to θ$

Proof

Step	Hyp	Ref	Expression
1		3imp.1	$⊢ φ \to (ψ \to (χ \to θ))$
2	1	com13	$⊢ χ \to (ψ \to (φ \to θ))$
3	2	3imp	$⊢ (χ \land ψ \land φ) \to θ$