Theorem mpbiran

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

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

Proof

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