Theorem bj-dfbi4

Description: Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019)

	Ref	Expression
Assertion	bj-dfbi4	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \neg \left(\phi \vee \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfbi3	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \neg \psi \right)\right)$$
2		pm4.56	$$⊢\left(\neg \phi \wedge \neg \psi \right)\leftrightarrow \neg \left(\phi \vee \psi \right)$$
3	2	orbi2i	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \neg \psi \right)\right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \neg \left(\phi \vee \psi \right)\right)$$
4	1 3	bitri	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \neg \left(\phi \vee \psi \right)\right)$$