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 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mtbii  329  mtbiri  330  sbn1  2144  axc10  2414  pwnss  5316  nsuceq0  6443  onssnel2i  6476  abnex  7757  ssonprc  7787  soseq  8158  dmtpos  8237  tfrlem15  8382  tz7.44-2  8397  tz7.48-3  8434  2pwuninel  9131  2pwne  9132  nnsdomg  9270  r111  9758  r1pwss  9767  wfelirr  9808  rankxplim3  9864  carduni  9987  alephle  10092  alephfp  10112  pwdjudom  10218  cfsuc  10260  fin23lem28  10343  fin23lem30  10345  isfin1-2  10388  ac5b  10481  zorn2lem4  10502  zorn2lem7  10505  cfpwsdom  10594  nd1  10597  nd2  10598  canthp1  10664  pwfseqlem1  10668  gchhar  10689  winalim2  10706  ltxrlt  11305  recgt0  12086  nnunb  12525  indstr  12966  wrdlen2i  15014  rlimno1  15742  lcmfnncl  16720  isprm2  16773  nprmdvds1  16798  divgcdodd  16802  coprm  16803  ramtcl2  17104  chnccat  18715  psgnunilem3  19624  torsubg  19982  prmcyg  20022  dprd2da  20172  prmirredlem  21686  pnfnei  23446  mnfnei  23447  1stccnp  23689  uzfbas  24125  ufinffr  24156  fin1aufil  24159  ovolunlem1a  25725  itg2gt0  25989  lgsquad2lem2  27622  dirith2  27765  noseponlem  27901  nosepssdm  27923  nodenselem8  27928  nolt02o  27932  nogt01o  27933  umgrnloop0  29567  usgrnloop0ALT  29666  nfrgr2v  30753  hon0  32275  ifeqeqx  33018  axsepg3ALT  35669  dfon2lem7  36367  bj-axc10v  37537  sbn1ALT  37602  bj-nsnid  37815  areacirclem4  38461  fdc  38496  dihglblem6  42214  sn-itrere  43377  sn-retire  43378  pellexlem6  43676  pw2f1ocnv  43879  wepwsolem  43884  inaex  45122  axc5c4c711toc5  45227  lptioo2  46462  lptioo1  46463  1neven  49154