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

Proof

Step	Hyp	Ref	Expression
1		pm2.27	$⊢ ⊤ \to ((⊤ \to φ) \to φ)$
2		pm2.27	$⊢ ((⊤ \to φ) \to φ) \to ((((⊤ \to φ) \to φ) \to ψ) \to ψ)$
3	1 2	syl	$⊢ ⊤ \to ((((⊤ \to φ) \to φ) \to ψ) \to ψ)$
4	3	mptru	$⊢ (((⊤ \to φ) \to φ) \to ψ) \to ψ$
5		antnestlaw3	$⊢ ((((⊤ \to φ) \to φ) \to ψ) \to ψ) \leftrightarrow ((((⊤ \to φ) \to ψ) \to φ) \to φ)$
6		antnestlaw1	$⊢ ((((⊤ \to φ) \to ψ) \to ψ) \to ψ) \leftrightarrow ((⊤ \to φ) \to ψ)$
7	6	imbi1i	$⊢ (((((⊤ \to φ) \to ψ) \to ψ) \to ψ) \to φ) \leftrightarrow (((⊤ \to φ) \to ψ) \to φ)$
8	7	imbi1i	$⊢ ((((((⊤ \to φ) \to ψ) \to ψ) \to ψ) \to φ) \to φ) \leftrightarrow ((((⊤ \to φ) \to ψ) \to φ) \to φ)$
9	5 8	bitr4i	$⊢ ((((⊤ \to φ) \to φ) \to ψ) \to ψ) \leftrightarrow ((((((⊤ \to φ) \to ψ) \to ψ) \to ψ) \to φ) \to φ)$
10		antnestlaw3	$⊢ ((((((⊤ \to φ) \to ψ) \to ψ) \to ψ) \to φ) \to φ) \leftrightarrow ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ)$
11	9 10	bitri	$⊢ ((((⊤ \to φ) \to φ) \to ψ) \to ψ) \leftrightarrow ((((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ)$
12	4 11	mpbi	$⊢ (((((⊤ \to φ) \to ψ) \to ψ) \to φ) \to ψ) \to ψ$

Metamath Proof Explorer

Theorem antnestALT

Proof