Theorem expandan

Description: Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		expandan.1	$$⊢\phi \leftrightarrow \psi$$
2		expandan.2	$$⊢\chi \leftrightarrow \theta$$
3	1 2	anbi12i	$$⊢\left(\phi \wedge \chi \right)\leftrightarrow \left(\psi \wedge \theta \right)$$
4		df-an	$$⊢\left(\psi \wedge \theta \right)\leftrightarrow \neg \left(\psi \to \neg \theta \right)$$
5	3 4	bitri	$$⊢\left(\phi \wedge \chi \right)\leftrightarrow \neg \left(\psi \to \neg \theta \right)$$