Theorem mpbirand

Description: Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		mpbirand.1	$$⊢\phi \to \chi$$
2		mpbirand.2	$$⊢\phi \to \left(\psi \leftrightarrow \left(\chi \wedge \theta \right)\right)$$
3	1	biantrurd	$$⊢\phi \to \left(\theta \leftrightarrow \left(\chi \wedge \theta \right)\right)$$
4	2 3	bitr4d	$$⊢\phi \to \left(\psi \leftrightarrow \theta \right)$$