Theorem mtoi 625

Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)

Hypotheses

Ref	Expression
mtoi.1	⊢ ¬ 𝜒
mtoi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtoi	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 ⊢ ¬ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → ¬ 𝜒)
3		mtoi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mtod 624	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 579  ax-in2 580

This theorem is referenced by:  mtbii  634  mtbiri  635  pwnss  3994  nsuceq0g  4245  reg2exmidlema  4350  ordsuc  4379  onnmin  4384  ssnel  4385  ordtri2or2exmid  4387  reg3exmidlemwe  4394  acexmidlemab  5646  reldmtpos  6018  dmtpos  6021  2pwuninelg  6048  onunsnss  6627  snon0  6645  exmidomni  6798  pr2ne  6820  ltexprlemdisj  7165  recexprlemdisj  7189  caucvgprlemnkj  7225  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemnjltk  7250  inelr  8061  rimul  8062  recgt0  8311  zfz1iso  10246  isprm2  11377  nprmdvds1  11399  divgcdodd  11400  coprm  11401  nninfalllem1  11899  nninfall  11900  nninfsellemqall  11907