Theorem 2falsed

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013) (Proof shortened by Wolf Lammen, 11-Apr-2024)

	Ref	Expression
Hypotheses	2falsed.1	⊢ ( 𝜑 → ¬ 𝜓 )
	2falsed.2	⊢ ( 𝜑 → ¬ 𝜒 )
Assertion	2falsed	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		2falsed.1	⊢ ( 𝜑 → ¬ 𝜓 )
2		2falsed.2	⊢ ( 𝜑 → ¬ 𝜒 )
3	1 2	2thd	⊢ ( 𝜑 → ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
4	3	con4bid	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )