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	⊢ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		simplim	⊢ ( ¬ ( ( ⊤ → 𝜑 ) → 𝜓 ) → ( ⊤ → 𝜑 ) )
2		conax1	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ¬ 𝜓 )
3		simplim	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) )
4	2 3	mtod	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ¬ ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) )
5		simplim	⊢ ( ¬ ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) )
6	4 5	syl	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) )
7	2 6	mtod	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ¬ ( ( ⊤ → 𝜑 ) → 𝜓 ) )
8	1 7	syl11	⊢ ( ⊤ → ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) )
9	8	mptru	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 )
10		conax1	⊢ ( ¬ ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → ¬ 𝜑 )
11	4 10	syl	⊢ ( ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) → ¬ 𝜑 )
12	9 11	pm2.65i	⊢ ¬ ¬ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 )
13	12	notnotri	⊢ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 )