Theorem resinsnlem

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

	Ref	Expression
Hypotheses	resinsnlem.1	⊢ ( 𝜑 → ( 𝜒 ↔ ¬ 𝜓 ) )
	resinsnlem.2	⊢ ( ¬ 𝜑 → 𝜒 )
Assertion	resinsnlem	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		resinsnlem.1	⊢ ( 𝜑 → ( 𝜒 ↔ ¬ 𝜓 ) )
2		resinsnlem.2	⊢ ( ¬ 𝜑 → 𝜒 )
3	1	con2bid	⊢ ( 𝜑 → ( 𝜓 ↔ ¬ 𝜒 ) )
4	3	biimpa	⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝜒 )
5	2	con1i	⊢ ( ¬ 𝜒 → 𝜑 )
6	5 3	syl	⊢ ( ¬ 𝜒 → ( 𝜓 ↔ ¬ 𝜒 ) )
7	6	ibir	⊢ ( ¬ 𝜒 → 𝜓 )
8	5 7	jca	⊢ ( ¬ 𝜒 → ( 𝜑 ∧ 𝜓 ) )
9	4 8	impbii	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ 𝜒 )