Metamath Proof Explorer

Theorem dfbi1ALTa

Description: Version of dfbi1ALT using T. for step 2 and shortened using a1i , a2i , and con4i . (Contributed by Eric Schmidt, 22-Oct-2025) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	dfbi1ALTa	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$

Proof

Step	Hyp	Ref	Expression
1		df-bi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
2		tru	$⊢ ⊤$
3		ax-1	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
4		df-bi	$⊢ \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
5	4	a1i	$⊢ \neg \neg ⊤ \to \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
6	5	con4i	$⊢ ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg ⊤$
7	6	a1i	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg ⊤)$
8	7	a2i	$⊢ (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))) \to (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg ⊤)$
9	3 8	ax-mp	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg ⊤$
10	9	con4i	$⊢ ⊤ \to (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))$
11	2 10	ax-mp	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))$
12	1 11	ax-mp	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$