Theorem mtoi 191

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 190	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  318  mtbiri  319  axc10  2405  ssdifsnOLD  4537  pwnss  5051  eunexOLD  5089  nsuceq0  6042  onssnel2i  6072  abnex  7225  ssonprc  7252  reldmtpos  7624  dmtpos  7628  tfrlem15  7753  tz7.44-2  7768  tz7.48-3  7804  2pwuninel  8383  2pwne  8384  nnsdomg  8487  r111  8914  r1pwss  8923  wfelirr  8964  rankxplim3  9020  carduni  9119  pr2ne  9140  alephle  9223  alephfp  9243  pwcdadom  9352  cfsuc  9393  fin23lem28  9476  fin23lem30  9478  isfin1-2  9521  ac5b  9614  zorn2lem4  9635  zorn2lem7  9638  cfpwsdom  9720  nd1  9723  nd2  9724  canthp1  9790  pwfseqlem1  9794  gchhar  9815  winalim2  9832  ltxrlt  10426  recgt0  11196  nnunb  11613  indstr  12038  wrdlen2i  14062  rlimno1  14760  lcmfnncl  15714  isprm2  15766  nprmdvds1  15788  divgcdodd  15792  coprm  15793  ramtcl2  16085  psgnunilem3  18266  torsubg  18609  prmcyg  18647  dprd2da  18794  prmirredlem  20200  pnfnei  21394  mnfnei  21395  1stccnp  21635  uzfbas  22071  ufinffr  22102  fin1aufil  22105  ovolunlem1a  23661  itg2gt0  23925  lgsquad2lem2  25522  dirith2  25629  umgrnloop0  26406  usgrnloop0ALT  26500  nfrgr2v  27652  hon0  29206  ifeqeqx  29908  dfon2lem7  32231  soseq  32292  noseponlem  32355  nosepssdm  32374  nodenselem8  32379  nolt02o  32383  bj-axc10v  33250  bj-nsnid  33630  areacirclem4  34045  fdc  34082  dihglblem6  37414  pellexlem6  38241  pw2f1ocnv  38446  wepwsolem  38454  axc5c4c711toc5  39441  lptioo2  40657  lptioo1  40658  1neven  42778