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  2113  axc10  2390  pwnss  5299  nsuceq0  6410  onssnel2i  6443  abnex  7712  ssonprc  7742  soseq  8111  dmtpos  8190  tfrlem15  8333  tz7.44-2  8348  tz7.48-3  8385  2pwuninel  9072  2pwne  9073  nnsdomg  9211  r111  9699  r1pwss  9708  wfelirr  9749  rankxplim3  9805  carduni  9905  alephle  10010  alephfp  10030  pwdjudom  10137  cfsuc  10179  fin23lem28  10262  fin23lem30  10264  isfin1-2  10307  ac5b  10400  zorn2lem4  10421  zorn2lem7  10424  cfpwsdom  10507  nd1  10510  nd2  10511  canthp1  10577  pwfseqlem1  10581  gchhar  10602  winalim2  10619  ltxrlt  11215  recgt0  11999  nnunb  12409  indstr  12841  wrdlen2i  14877  rlimno1  15589  lcmfnncl  16568  isprm2  16621  nprmdvds1  16645  divgcdodd  16649  coprm  16650  ramtcl2  16951  chnccat  18561  psgnunilem3  19437  torsubg  19795  prmcyg  19835  dprd2da  19985  prmirredlem  21439  pnfnei  23176  mnfnei  23177  1stccnp  23418  uzfbas  23854  ufinffr  23885  fin1aufil  23888  ovolunlem1a  25465  itg2gt0  25729  lgsquad2lem2  27364  dirith2  27507  noseponlem  27644  nosepssdm  27666  nodenselem8  27671  nolt02o  27675  nogt01o  27676  umgrnloop0  29194  usgrnloop0ALT  29290  nfrgr2v  30359  hon0  31881  ifeqeqx  32629  axsepg2ALT  35260  dfon2lem7  36003  bj-axc10v  37041  sbn1ALT  37106  bj-nsnid  37318  areacirclem4  37962  fdc  37996  dihglblem6  41716  sn-itrere  42858  sn-retire  42859  pellexlem6  43191  pw2f1ocnv  43394  wepwsolem  43399  inaex  44653  axc5c4c711toc5  44758  lptioo2  45991  lptioo1  45992  1neven  48598