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	$⊢ (((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ$

Proof

Step	Hyp	Ref	Expression
1		simplim	$⊢ \neg ((⊤ \to φ) \to ψ) \to (⊤ \to φ)$
2		conax1	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to \neg ψ$
3		simplim	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to (((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ)$
4	2 3	mtod	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to \neg ((((⊤ \to φ) \to ψ) \to ψ) \to φ)$
5		simplim	$⊢ \neg ((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to (((⊤ \to φ) \to ψ) \to ψ)$
6	4 5	syl	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to (((⊤ \to φ) \to ψ) \to ψ)$
7	2 6	mtod	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to \neg ((⊤ \to φ) \to ψ)$
8	1 7	syl11	$⊢ ⊤ \to (\neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to φ)$
9	8	mptru	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to φ$
10		conax1	$⊢ \neg ((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to \neg φ$
11	4 10	syl	$⊢ \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ) \to \neg φ$
12	9 11	pm2.65i	$⊢ \neg \neg ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ)$
13	12	notnotri	$⊢ (((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ$

Metamath Proof Explorer

Theorem antnest

Proof