Theorem mtoi 199

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 198	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  326  mtbiri  327  sbn1  2108  axc10  2383  pwnss  5291  nsuceq0  6392  onssnel2i  6425  abnex  7693  ssonprc  7723  soseq  8092  dmtpos  8171  tfrlem15  8314  tz7.44-2  8329  tz7.48-3  8366  2pwuninel  9049  2pwne  9050  nnsdomg  9188  r111  9671  r1pwss  9680  wfelirr  9721  rankxplim3  9777  carduni  9877  alephle  9982  alephfp  10002  pwdjudom  10109  cfsuc  10151  fin23lem28  10234  fin23lem30  10236  isfin1-2  10279  ac5b  10372  zorn2lem4  10393  zorn2lem7  10396  cfpwsdom  10478  nd1  10481  nd2  10482  canthp1  10548  pwfseqlem1  10552  gchhar  10573  winalim2  10590  ltxrlt  11186  recgt0  11970  nnunb  12380  indstr  12817  wrdlen2i  14849  rlimno1  15561  lcmfnncl  16540  isprm2  16593  nprmdvds1  16617  divgcdodd  16621  coprm  16622  ramtcl2  16923  psgnunilem3  19375  torsubg  19733  prmcyg  19773  dprd2da  19923  prmirredlem  21379  pnfnei  23105  mnfnei  23106  1stccnp  23347  uzfbas  23783  ufinffr  23814  fin1aufil  23817  ovolunlem1a  25395  itg2gt0  25659  lgsquad2lem2  27294  dirith2  27437  noseponlem  27574  nosepssdm  27596  nodenselem8  27601  nolt02o  27605  nogt01o  27606  umgrnloop0  29054  usgrnloop0ALT  29150  nfrgr2v  30216  hon0  31737  ifeqeqx  32486  axsepg2ALT  35050  dfon2lem7  35767  bj-axc10v  36771  sbn1ALT  36836  bj-nsnid  37048  areacirclem4  37695  fdc  37729  dihglblem6  41323  sn-itrere  42465  sn-retire  42466  pellexlem6  42811  pw2f1ocnv  43014  wepwsolem  43019  inaex  44274  axc5c4c711toc5  44379  lptioo2  45616  lptioo1  45617  1neven  48226