Theorem antnestALT

Description: Alternative proof of antnest from the valid schema ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) using laws of nested antecedents. Our proof uses only the laws antnestlaw1 and antnestlaw3 . (Contributed by Adrian Ducourtial, 5-Dec-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	antnestALT	⊢ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		pm2.27	⊢ ( ⊤ → ( ( ⊤ → 𝜑 ) → 𝜑 ) )
2		pm2.27	⊢ ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) )
3	1 2	syl	⊢ ( ⊤ → ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) )
4	3	mptru	⊢ ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 )
5		antnestlaw3	⊢ ( ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) ↔ ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜑 ) → 𝜑 ) )
6		antnestlaw1	⊢ ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜓 ) ↔ ( ( ⊤ → 𝜑 ) → 𝜓 ) )
7	6	imbi1i	⊢ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) ↔ ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜑 ) )
8	7	imbi1i	⊢ ( ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜑 ) ↔ ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜑 ) → 𝜑 ) )
9	5 8	bitr4i	⊢ ( ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) ↔ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜑 ) )
10		antnestlaw3	⊢ ( ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜑 ) ↔ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) )
11	9 10	bitri	⊢ ( ( ( ( ( ⊤ → 𝜑 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) ↔ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 ) )
12	4 11	mpbi	⊢ ( ( ( ( ( ( ⊤ → 𝜑 ) → 𝜓 ) → 𝜓 ) → 𝜑 ) → 𝜓 ) → 𝜓 )