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

Metamath Proof Explorer

Theorem mtbid

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses mtbid.min ⊢ φ → ¬ ψ
mtbid.maj ⊢ φ → ψ ↔ χ
Assertion mtbid ⊢ φ → ¬ χ

Proof

Step Hyp Ref Expression
1 mtbid.min ⊢ φ → ¬ ψ
2 mtbid.maj ⊢ φ → ψ ↔ χ
3 2 biimprd ⊢ φ → χ → ψ
4 1 3 mtod ⊢ φ → ¬ χ