Theorem antnest

Description: Suppose ph , ps are distinct atomic propositional formulas, and let _G be the smallest class of formulas for which T. e.G and ( ch -> ph ) , ( ch -> ps ) e. G for ch e.G . The present theorem is then an element of G , and the implications occurring in the theorem are in one-to-one correspondence with the formulas in _G up to logical equivalence. In particular, the theorem itself is equivalent to T. e. _G . (Contributed by Adrian Ducourtial, 2-Oct-2025)

	Ref	Expression
Assertion	antnest	|- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		simplim	|- ( -. ( ( T. -> ph ) -> ps ) -> ( T. -> ph ) )
2		conax1	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> -. ps )
3		simplim	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) )
4	2 3	mtod	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> -. ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) )
5		simplim	|- ( -. ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ( ( ( T. -> ph ) -> ps ) -> ps ) )
6	4 5	syl	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> ( ( ( T. -> ph ) -> ps ) -> ps ) )
7	2 6	mtod	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> -. ( ( T. -> ph ) -> ps ) )
8	1 7	syl11	|- ( T. -> ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> ph ) )
9	8	mptru	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> ph )
10		conax1	|- ( -. ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> -. ph )
11	4 10	syl	|- ( -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) -> -. ph )
12	9 11	pm2.65i	|- -. -. ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )
13	12	notnotri	|- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )