Theorem biimpor

Description: A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017)

	Ref	Expression
Assertion	biimpor	$$⊢\left(\left(\phi \leftrightarrow \psi \right)\to \chi \right)\leftrightarrow \left(\left(\neg \phi \leftrightarrow \psi \right)\vee \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		imor	$$⊢\left(\left(\phi \leftrightarrow \psi \right)\to \chi \right)\leftrightarrow \left(\neg \left(\phi \leftrightarrow \psi \right)\vee \chi \right)$$
2		notbinot2	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\neg \phi \leftrightarrow \psi \right)$$
3	2	orbi1i	$$⊢\left(\neg \left(\phi \leftrightarrow \psi \right)\vee \chi \right)\leftrightarrow \left(\left(\neg \phi \leftrightarrow \psi \right)\vee \chi \right)$$
4	1 3	bitri	$$⊢\left(\left(\phi \leftrightarrow \psi \right)\to \chi \right)\leftrightarrow \left(\left(\neg \phi \leftrightarrow \psi \right)\vee \chi \right)$$