Metamath Proof Explorer


Theorem mtbi

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994) (Proof shortened by Wolf Lammen, 25-Oct-2012)

Ref Expression
Hypotheses mtbi.1 ¬φ
mtbi.2 φψ
Assertion mtbi ¬ψ

Proof

Step Hyp Ref Expression
1 mtbi.1 ¬φ
2 mtbi.2 φψ
3 2 biimpri ψφ
4 1 3 mto ¬ψ