Theorem mtoi 190

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 189	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  317  mtbiri  318  axc10  2426  ssdifsnOLD  4508  pwnss  5020  eunex  5057  nsuceq0  6016  onssnel2i  6049  abnex  7193  ssonprc  7220  reldmtpos  7593  dmtpos  7597  tfrlem15  7722  tz7.44-2  7737  tz7.48-3  7773  2pwuninel  8352  2pwne  8353  nnsdomg  8456  r111  8883  r1pwss  8892  wfelirr  8933  rankxplim3  8989  carduni  9088  pr2ne  9109  alephle  9192  alephfp  9212  pwcdadom  9321  cfsuc  9362  fin23lem28  9445  fin23lem30  9447  isfin1-2  9490  ac5b  9583  zorn2lem4  9604  zorn2lem7  9607  cfpwsdom  9689  nd1  9692  nd2  9693  canthp1  9759  pwfseqlem1  9763  gchhar  9784  winalim2  9801  ltxrlt  10391  recgt0  11150  nnunb  11553  indstr  11973  wrdlen2i  13909  rlimno1  14605  lcmfnncl  15559  isprm2  15611  nprmdvds1  15633  divgcdodd  15637  coprm  15638  ramtcl2  15930  psgnunilem3  18115  torsubg  18456  prmcyg  18494  dprd2da  18641  prmirredlem  20047  pnfnei  21236  mnfnei  21237  1stccnp  21477  uzfbas  21913  ufinffr  21944  fin1aufil  21947  ovolunlem1a  23475  itg2gt0  23739  lgsquad2lem2  25322  dirith2  25429  umgrnloop0  26216  usgrnloop0ALT  26310  nfrgr2v  27445  hon0  28978  ifeqeqx  29684  dfon2lem7  32012  soseq  32073  noseponlem  32136  nosepssdm  32155  nodenselem8  32160  nolt02o  32164  bj-axc10v  33030  bj-eunex  33111  areacirclem4  33813  fdc  33850  dihglblem6  37119  pellexlem6  37898  pw2f1ocnv  38103  wepwsolem  38111  axc5c4c711toc5  39100  lptioo2  40341  lptioo1  40342  1neven  42498