Metamath Proof Explorer

Theorem expcomdg

Description: Biconditional form of expcomd . (Contributed by Alan Sare, 22-Jul-2012) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		ancomst	$⊢ ((ψ \land χ) \to θ) \leftrightarrow ((χ \land ψ) \to θ)$
2		impexp	$⊢ ((χ \land ψ) \to θ) \leftrightarrow (χ \to (ψ \to θ))$
3	1 2	bitri	$⊢ ((ψ \land χ) \to θ) \leftrightarrow (χ \to (ψ \to θ))$
4	3	imbi2i	$⊢ (φ \to ((ψ \land χ) \to θ)) \leftrightarrow (φ \to (χ \to (ψ \to θ)))$