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  2112  axc10  2387  pwnss  5295  nsuceq0  6400  onssnel2i  6433  abnex  7700  ssonprc  7730  soseq  8099  dmtpos  8178  tfrlem15  8321  tz7.44-2  8336  tz7.48-3  8373  2pwuninel  9058  2pwne  9059  nnsdomg  9197  r111  9685  r1pwss  9694  wfelirr  9735  rankxplim3  9791  carduni  9891  alephle  9996  alephfp  10016  pwdjudom  10123  cfsuc  10165  fin23lem28  10248  fin23lem30  10250  isfin1-2  10293  ac5b  10386  zorn2lem4  10407  zorn2lem7  10410  cfpwsdom  10493  nd1  10496  nd2  10497  canthp1  10563  pwfseqlem1  10567  gchhar  10588  winalim2  10605  ltxrlt  11201  recgt0  11985  nnunb  12395  indstr  12827  wrdlen2i  14863  rlimno1  15575  lcmfnncl  16554  isprm2  16607  nprmdvds1  16631  divgcdodd  16635  coprm  16636  ramtcl2  16937  chnccat  18547  psgnunilem3  19423  torsubg  19781  prmcyg  19821  dprd2da  19971  prmirredlem  21425  pnfnei  23162  mnfnei  23163  1stccnp  23404  uzfbas  23840  ufinffr  23871  fin1aufil  23874  ovolunlem1a  25451  itg2gt0  25715  lgsquad2lem2  27350  dirith2  27493  noseponlem  27630  nosepssdm  27652  nodenselem8  27657  nolt02o  27661  nogt01o  27662  umgrnloop0  29131  usgrnloop0ALT  29227  nfrgr2v  30296  hon0  31817  ifeqeqx  32566  axsepg2ALT  35188  dfon2lem7  35930  bj-axc10v  36937  sbn1ALT  37002  bj-nsnid  37214  areacirclem4  37851  fdc  37885  dihglblem6  41539  sn-itrere  42685  sn-retire  42686  pellexlem6  43018  pw2f1ocnv  43221  wepwsolem  43226  inaex  44480  axc5c4c711toc5  44585  lptioo2  45819  lptioo1  45820  1neven  48426