Theorem ibdr

Description: Reverse of ibd . (Contributed by Rodolfo Medina, 30-Sep-2010)

	Ref	Expression
Hypothesis	ibdr.1	$$⊢\phi \to \left(\chi \to \left(\psi \leftrightarrow \chi \right)\right)$$
Assertion	ibdr	$$⊢\phi \to \left(\chi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ibdr.1	$$⊢\phi \to \left(\chi \to \left(\psi \leftrightarrow \chi \right)\right)$$
2	1	bicomdd	$$⊢\phi \to \left(\chi \to \left(\chi \leftrightarrow \psi \right)\right)$$
3	2	ibd	$$⊢\phi \to \left(\chi \to \psi \right)$$