Theorem dfbi1ALTb

Description: Further shorten dfbi1ALTa using simprimi . (Contributed by Eric Schmidt, 22-Oct-2025) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	dfbi1ALTb	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bi	⊢ ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) )
2		df-bi	⊢ ¬ ( ( ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) ) → ¬ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) )
3	2	simprimi	⊢ ( ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) )
4	1 3	ax-mp	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )