Theorem antnestlaw3lem

Description: Lemma for antnestlaw3 . (Contributed by Adrian Ducourtial, 5-Dec-2025)

	Ref	Expression
Assertion	antnestlaw3lem	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ( ( ( ph -> ch ) -> ps ) -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		conax1	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ch )
2		simplim	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> ( ( ph -> ps ) -> ch ) )
3	1 2	mtod	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ( ph -> ps ) )
4		simplim	|- ( -. ( ph -> ps ) -> ph )
5	3 4	syl	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> ph )
6	5 1	jcnd	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ( ph -> ch ) )
7	6	pm2.21d	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> ( ( ph -> ch ) -> ps ) )
8		conax1	|- ( -. ( ph -> ps ) -> -. ps )
9	3 8	syl	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ps )
10	7 9	jcnd	|- ( -. ( ( ( ph -> ps ) -> ch ) -> ch ) -> -. ( ( ( ph -> ch ) -> ps ) -> ps ) )