This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → ψ ↔ χ