Theorem impcon4bid

Description: A variation on impbid with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009)

	Ref	Expression
Hypotheses	impcon4bid.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
	impcon4bid.2	$$⊢\phi \to \left(\neg \psi \to \neg \chi \right)$$
Assertion	impcon4bid	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		impcon4bid.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		impcon4bid.2	$$⊢\phi \to \left(\neg \psi \to \neg \chi \right)$$
3	2	con4d	$$⊢\phi \to \left(\chi \to \psi \right)$$
4	1 3	impbid	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$