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 φ ψ χ