Theorem bibi2i

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 16-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		bibi2i.1	$$⊢\phi \leftrightarrow \psi$$
2		id	$$⊢\left(\chi \leftrightarrow \phi \right)\to \left(\chi \leftrightarrow \phi \right)$$
3	2 1	bitrdi	$$⊢\left(\chi \leftrightarrow \phi \right)\to \left(\chi \leftrightarrow \psi \right)$$
4		id	$$⊢\left(\chi \leftrightarrow \psi \right)\to \left(\chi \leftrightarrow \psi \right)$$
5	4 1	bitr4di	$$⊢\left(\chi \leftrightarrow \psi \right)\to \left(\chi \leftrightarrow \phi \right)$$
6	3 5	impbii	$$⊢\left(\chi \leftrightarrow \phi \right)\leftrightarrow \left(\chi \leftrightarrow \psi \right)$$