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	|- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		pm2.27	|- ( T. -> ( ( T. -> ph ) -> ph ) )
2		pm2.27	|- ( ( ( T. -> ph ) -> ph ) -> ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) )
3	1 2	syl	|- ( T. -> ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) )
4	3	mptru	|- ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps )
5		antnestlaw3	|- ( ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) <-> ( ( ( ( T. -> ph ) -> ps ) -> ph ) -> ph ) )
6		antnestlaw1	|- ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ps ) <-> ( ( T. -> ph ) -> ps ) )
7	6	imbi1i	|- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ps ) -> ph ) <-> ( ( ( T. -> ph ) -> ps ) -> ph ) )
8	7	imbi1i	|- ( ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ps ) -> ph ) -> ph ) <-> ( ( ( ( T. -> ph ) -> ps ) -> ph ) -> ph ) )
9	5 8	bitr4i	|- ( ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) <-> ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ps ) -> ph ) -> ph ) )
10		antnestlaw3	|- ( ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ps ) -> ph ) -> ph ) <-> ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) )
11	9 10	bitri	|- ( ( ( ( ( T. -> ph ) -> ph ) -> ps ) -> ps ) <-> ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps ) )
12	4 11	mpbi	|- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )