Theorem resinsnlem

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

	Ref	Expression
Hypotheses	resinsnlem.1	|- ( ph -> ( ch <-> -. ps ) )
	resinsnlem.2	|- ( -. ph -> ch )
Assertion	resinsnlem	|- ( ( ph /\ ps ) <-> -. ch )

Proof

Step	Hyp	Ref	Expression
1		resinsnlem.1	|- ( ph -> ( ch <-> -. ps ) )
2		resinsnlem.2	|- ( -. ph -> ch )
3	1	con2bid	|- ( ph -> ( ps <-> -. ch ) )
4	3	biimpa	|- ( ( ph /\ ps ) -> -. ch )
5	2	con1i	|- ( -. ch -> ph )
6	5 3	syl	|- ( -. ch -> ( ps <-> -. ch ) )
7	6	ibir	|- ( -. ch -> ps )
8	5 7	jca	|- ( -. ch -> ( ph /\ ps ) )
9	4 8	impbii	|- ( ( ph /\ ps ) <-> -. ch )