Theorem mpbiran2

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996)

	Ref	Expression
Hypotheses	mpbiran2.1	$$⊢\chi$$
	mpbiran2.2	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
Assertion	mpbiran2	$$⊢\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		mpbiran2.1	$$⊢\chi$$
2		mpbiran2.2	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
3	2	biancomi	$$⊢\phi \leftrightarrow \left(\chi \wedge \psi \right)$$
4	1 3	mpbiran	$$⊢\phi \leftrightarrow \psi$$