Theorem antnest 35673

Description: Suppose 𝜑, 𝜓 are distinct atomic propositional formulas, and let Γ be the smallest class of formulas for which ⊤ ∈ Γ and (𝜒 → 𝜑), (𝜒 → 𝜓) ∈ Γ for 𝜒 ∈ Γ. The present theorem is then an element of Γ, and the implications occurring in the theorem are in one-to-one correspondence with the formulas in Γ up to logical equivalence. In particular, the theorem itself is equivalent to ⊤ ∈ Γ. (Contributed by Adrian Ducourtial, 2-Oct-2025.)

Assertion

Ref	Expression
antnest	⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)

Proof of Theorem antnest

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

Syntax hints:  ¬ wn 3   → wi 4  ⊤wtru 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-tru 1539

This theorem is referenced by: (None)