Theorem mtoi 198

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 197	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  325  mtbiri  326  sbn1  2105  axc10  2384  pwnss  5349  nsuceq0  6447  onssnel2i  6481  abnex  7743  ssonprc  7774  soseq  8144  dmtpos  8222  tfrlem15  8391  tz7.44-2  8406  tz7.48-3  8443  2pwuninel  9131  2pwne  9132  nnsdomg  9301  nnsdomgOLD  9302  r111  9769  r1pwss  9778  wfelirr  9819  rankxplim3  9875  carduni  9975  pr2neOLD  9999  alephle  10082  alephfp  10102  pwdjudom  10210  cfsuc  10251  fin23lem28  10334  fin23lem30  10336  isfin1-2  10379  ac5b  10472  zorn2lem4  10493  zorn2lem7  10496  cfpwsdom  10578  nd1  10581  nd2  10582  canthp1  10648  pwfseqlem1  10652  gchhar  10673  winalim2  10690  ltxrlt  11283  recgt0  12059  nnunb  12467  indstr  12899  wrdlen2i  14892  rlimno1  15599  lcmfnncl  16565  isprm2  16618  nprmdvds1  16642  divgcdodd  16646  coprm  16647  ramtcl2  16943  psgnunilem3  19363  torsubg  19721  prmcyg  19761  dprd2da  19911  prmirredlem  21041  pnfnei  22723  mnfnei  22724  1stccnp  22965  uzfbas  23401  ufinffr  23432  fin1aufil  23435  ovolunlem1a  25012  itg2gt0  25277  lgsquad2lem2  26885  dirith2  27028  noseponlem  27164  nosepssdm  27186  nodenselem8  27191  nolt02o  27195  nogt01o  27196  umgrnloop0  28366  usgrnloop0ALT  28459  nfrgr2v  29522  hon0  31041  ifeqeqx  31769  dfon2lem7  34756  bj-axc10v  35666  sbn1ALT  35732  bj-nsnid  35946  areacirclem4  36574  fdc  36608  dihglblem6  40206  sn-inelr  41339  itrere  41340  retire  41341  pellexlem6  41562  pw2f1ocnv  41766  wepwsolem  41774  inaex  43046  axc5c4c711toc5  43151  lptioo2  44337  lptioo1  44338  1neven  46820