Theorem impbidd

Description: Deduce an equivalence from two implications. Double deduction associated with impbi and impbii . Deduction associated with impbid . (Contributed by Rodolfo Medina, 12-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		impbidd.1	$$⊢\phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
2		impbidd.2	$$⊢\phi \to \left(\psi \to \left(\theta \to \chi \right)\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	syl6c	$$⊢\phi \to \left(\psi \to \left(\chi \leftrightarrow \theta \right)\right)$$