Metamath Proof Explorer


Theorem con2bid

Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995)

Ref Expression
Hypothesis con2bid.1 φ ψ ¬ χ
Assertion con2bid φ χ ¬ ψ

Proof

Step Hyp Ref Expression
1 con2bid.1 φ ψ ¬ χ
2 con2bi χ ¬ ψ ψ ¬ χ
3 1 2 sylibr φ χ ¬ ψ