Theorem impbid2

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007) (Proof shortened by Wolf Lammen, 27-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		impbid2.1	$$⊢\psi \to \chi$$
2		impbid2.2	$$⊢\phi \to \left(\chi \to \psi \right)$$
3	2 1	impbid1	$$⊢\phi \to \left(\chi \leftrightarrow \psi \right)$$
4	3	bicomd	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$