Theorem impbid21d

Description: Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		impbid21d.1	$$⊢\psi \to \left(\chi \to \theta \right)$$
2		impbid21d.2	$$⊢\phi \to \left(\theta \to \chi \right)$$
3		impbi	$$⊢\left(\chi \to \theta \right)\to \left(\left(\theta \to \chi \right)\to \left(\chi \leftrightarrow \theta \right)\right)$$
4	1 2 3	syl2imc	$$⊢\phi \to \left(\psi \to \left(\chi \leftrightarrow \theta \right)\right)$$