Theorem resinsnlem

Description: Lemma for resinsnALT . (Contributed by Zhi Wang, 6-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		resinsnlem.1	$$⊢\phi \to \left(\chi \leftrightarrow \neg \psi \right)$$
2		resinsnlem.2	$$⊢\neg \phi \to \chi$$
3	1	con2bid	$$⊢\phi \to \left(\psi \leftrightarrow \neg \chi \right)$$
4	3	biimpa	$$⊢\left(\phi \wedge \psi \right)\to \neg \chi$$
5	2	con1i	$$⊢\neg \chi \to \phi$$
6	5 3	syl	$$⊢\neg \chi \to \left(\psi \leftrightarrow \neg \chi \right)$$
7	6	ibir	$$⊢\neg \chi \to \psi$$
8	5 7	jca	$$⊢\neg \chi \to \left(\phi \wedge \psi \right)$$
9	4 8	impbii	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \neg \chi$$