Theorem exbir

Description: Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD . (Contributed by Alan Sare, 31-Dec-2011)

	Ref	Expression
Assertion	exbir	|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		biimpr	|- ( ( ch <-> th ) -> ( th -> ch ) )
2	1	imim2i	|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ( ph /\ ps ) -> ( th -> ch ) ) )
3	2	expd	|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )