Theorem bianbi

Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		bianbi.1	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
2		bianbi.2	$$⊢\psi \leftrightarrow \theta$$
3	2	anbi1i	$$⊢\left(\psi \wedge \chi \right)\leftrightarrow \left(\theta \wedge \chi \right)$$
4	1 3	bitri	$$⊢\phi \leftrightarrow \left(\theta \wedge \chi \right)$$