Theorem mtoi 202

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 11	. 2 ⊢ (𝜑 → ¬ 𝜒)
3		mtoi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mtbii  329  mtbiri  330  sbn1  2148  axc10  2423  pwnss  5323  nsuceq0  6447  onssnel2i  6480  abnex  7755  ssonprc  7785  soseq  8154  dmtpos  8233  tfrlem15  8378  tz7.44-2  8393  tz7.48-3  8430  2pwuninel  9119  2pwne  9120  nnsdomg  9258  r111  9746  r1pwss  9755  wfelirr  9796  rankxplim3  9852  carduni  9966  alephle  10071  alephfp  10091  pwdjudom  10197  cfsuc  10240  fin23lem28  10323  fin23lem30  10325  isfin1-2  10368  ac5b  10461  zorn2lem4  10482  zorn2lem7  10485  cfpwsdom  10568  nd1  10571  nd2  10572  canthp1  10638  pwfseqlem1  10642  gchhar  10663  winalim2  10680  ltxrlt  11279  recgt0  12060  nnunb  12499  indstr  12939  wrdlen2i  14978  rlimno1  15704  lcmfnncl  16686  isprm2  16739  nprmdvds1  16764  divgcdodd  16768  coprm  16769  ramtcl2  17070  chnccat  18681  psgnunilem3  19565  torsubg  19923  prmcyg  19963  dprd2da  20113  prmirredlem  21590  pnfnei  23345  mnfnei  23346  1stccnp  23587  uzfbas  24023  ufinffr  24054  fin1aufil  24057  ovolunlem1a  25623  itg2gt0  25887  lgsquad2lem2  27514  dirith2  27657  noseponlem  27793  nosepssdm  27815  nodenselem8  27820  nolt02o  27824  nogt01o  27825  umgrnloop0  29399  usgrnloop0ALT  29495  nfrgr2v  30563  hon0  32085  ifeqeqx  32828  axsepg3ALT  35477  dfon2lem7  36177  bj-axc10v  37316  sbn1ALT  37381  bj-nsnid  37593  areacirclem4  38249  fdc  38283  dihglblem6  42003  sn-itrere  43151  sn-retire  43152  pellexlem6  43452  pw2f1ocnv  43655  wepwsolem  43660  inaex  44898  axc5c4c711toc5  45003  lptioo2  46238  lptioo1  46239  1neven  48891