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  5290  nsuceq0  6403  onssnel2i  6436  abnex  7705  ssonprc  7735  soseq  8103  dmtpos  8182  tfrlem15  8325  tz7.44-2  8340  tz7.48-3  8377  2pwuninel  9064  2pwne  9065  nnsdomg  9203  r111  9693  r1pwss  9702  wfelirr  9743  rankxplim3  9799  carduni  9899  alephle  10004  alephfp  10024  pwdjudom  10131  cfsuc  10173  fin23lem28  10256  fin23lem30  10258  isfin1-2  10301  ac5b  10394  zorn2lem4  10415  zorn2lem7  10418  cfpwsdom  10501  nd1  10504  nd2  10505  canthp1  10571  pwfseqlem1  10575  gchhar  10596  winalim2  10613  ltxrlt  11210  recgt0  11995  nnunb  12427  indstr  12860  wrdlen2i  14898  rlimno1  15610  lcmfnncl  16592  isprm2  16645  nprmdvds1  16670  divgcdodd  16674  coprm  16675  ramtcl2  16976  chnccat  18586  psgnunilem3  19465  torsubg  19823  prmcyg  19863  dprd2da  20013  prmirredlem  21465  pnfnei  23198  mnfnei  23199  1stccnp  23440  uzfbas  23876  ufinffr  23907  fin1aufil  23910  ovolunlem1a  25476  itg2gt0  25740  lgsquad2lem2  27365  dirith2  27508  noseponlem  27645  nosepssdm  27667  nodenselem8  27672  nolt02o  27676  nogt01o  27677  umgrnloop0  29195  usgrnloop0ALT  29291  nfrgr2v  30360  hon0  31882  ifeqeqx  32630  axsepg2ALT  35245  dfon2lem7  35988  bj-axc10v  37119  sbn1ALT  37184  bj-nsnid  37396  areacirclem4  38049  fdc  38083  dihglblem6  41803  sn-itrere  42950  sn-retire  42951  pellexlem6  43283  pw2f1ocnv  43486  wepwsolem  43491  inaex  44745  axc5c4c711toc5  44850  lptioo2  46082  lptioo1  46083  1neven  48729