Theorem mtoi 201

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 200	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  328  mtbiri  329  sbn1  2131  axc10  2406  pwnss  5298  nsuceq0  6416  onssnel2i  6449  abnex  7725  ssonprc  7755  soseq  8123  dmtpos  8202  tfrlem15  8347  tz7.44-2  8362  tz7.48-3  8399  2pwuninel  9089  2pwne  9090  nnsdomg  9228  r111  9719  r1pwss  9728  wfelirr  9769  rankxplim3  9825  carduni  9925  alephle  10030  alephfp  10050  pwdjudom  10157  cfsuc  10200  fin23lem28  10283  fin23lem30  10285  isfin1-2  10328  ac5b  10421  zorn2lem4  10442  zorn2lem7  10445  cfpwsdom  10528  nd1  10531  nd2  10532  canthp1  10598  pwfseqlem1  10602  gchhar  10623  winalim2  10640  ltxrlt  11239  recgt0  12023  nnunb  12463  indstr  12903  wrdlen2i  14941  rlimno1  15653  lcmfnncl  16635  isprm2  16688  nprmdvds1  16713  divgcdodd  16717  coprm  16718  ramtcl2  17019  chnccat  18630  psgnunilem3  19508  torsubg  19866  prmcyg  19906  dprd2da  20056  prmirredlem  21493  pnfnei  23249  mnfnei  23250  1stccnp  23491  uzfbas  23927  ufinffr  23958  fin1aufil  23961  ovolunlem1a  25527  itg2gt0  25791  lgsquad2lem2  27415  dirith2  27558  noseponlem  27694  nosepssdm  27716  nodenselem8  27721  nolt02o  27725  nogt01o  27726  umgrnloop0  29245  usgrnloop0ALT  29341  nfrgr2v  30409  hon0  31931  ifeqeqx  32679  axsepg3ALT  35383  dfon2lem7  36075  bj-axc10v  37216  sbn1ALT  37281  bj-nsnid  37493  areacirclem4  38148  fdc  38182  dihglblem6  41902  sn-itrere  43048  sn-retire  43049  pellexlem6  43349  pw2f1ocnv  43552  wepwsolem  43557  inaex  44811  axc5c4c711toc5  44916  lptioo2  46145  lptioo1  46146  1neven  48798