Theorem impbid1

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007)

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

Proof

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