3impexp

Description: Version of impexp for a triple conjunction. (Contributed by Alan Sare, 31-Dec-2011)

		Ref	Expression
	Assertion	3impexp	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$

Step	Hyp	Ref	Expression
1		id	$⊢ ((φ \land ψ \land χ) \to θ) \to ((φ \land ψ \land χ) \to θ)$
2	1	3expd	$⊢ ((φ \land ψ \land χ) \to θ) \to (φ \to (ψ \to (χ \to θ)))$
3		id	$⊢ (φ \to (ψ \to (χ \to θ))) \to (φ \to (ψ \to (χ \to θ)))$
4	3	3impd	$⊢ (φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ \land χ) \to θ)$
5	2 4	impbii	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$

Metamath Proof Explorer