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	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bi	⊢ ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) )
2		tru	⊢ ⊤
3		ax-1	⊢ ( ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) → ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) ) )
4		df-bi	⊢ ¬ ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) )
5	4	a1i	⊢ ( ¬ ¬ ⊤ → ¬ ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) ) )
6	5	con4i	⊢ ( ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) ) → ¬ ⊤ )
7	6	a1i	⊢ ( ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) → ( ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) ) → ¬ ⊤ ) )
8	7	a2i	⊢ ( ( ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) → ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) ) ) → ( ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) → ¬ ⊤ ) )
9	3 8	ax-mp	⊢ ( ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) → ¬ ⊤ )
10	9	con4i	⊢ ( ⊤ → ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) )
11	2 10	ax-mp	⊢ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) )
12	1 11	ax-mp	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )