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  2107  axc10  2390  pwnss  5352  nsuceq0  6467  onssnel2i  6501  abnex  7777  ssonprc  7807  soseq  8184  dmtpos  8263  tfrlem15  8432  tz7.44-2  8447  tz7.48-3  8484  2pwuninel  9172  2pwne  9173  nnsdomg  9335  nnsdomgOLD  9336  r111  9815  r1pwss  9824  wfelirr  9865  rankxplim3  9921  carduni  10021  pr2neOLD  10045  alephle  10128  alephfp  10148  pwdjudom  10255  cfsuc  10297  fin23lem28  10380  fin23lem30  10382  isfin1-2  10425  ac5b  10518  zorn2lem4  10539  zorn2lem7  10542  cfpwsdom  10624  nd1  10627  nd2  10628  canthp1  10694  pwfseqlem1  10698  gchhar  10719  winalim2  10736  ltxrlt  11331  recgt0  12113  nnunb  12522  indstr  12958  wrdlen2i  14981  rlimno1  15690  lcmfnncl  16666  isprm2  16719  nprmdvds1  16743  divgcdodd  16747  coprm  16748  ramtcl2  17049  psgnunilem3  19514  torsubg  19872  prmcyg  19912  dprd2da  20062  prmirredlem  21483  pnfnei  23228  mnfnei  23229  1stccnp  23470  uzfbas  23906  ufinffr  23937  fin1aufil  23940  ovolunlem1a  25531  itg2gt0  25795  lgsquad2lem2  27429  dirith2  27572  noseponlem  27709  nosepssdm  27731  nodenselem8  27736  nolt02o  27740  nogt01o  27741  umgrnloop0  29126  usgrnloop0ALT  29222  nfrgr2v  30291  hon0  31812  ifeqeqx  32555  axsepg2ALT  35097  dfon2lem7  35790  bj-axc10v  36794  sbn1ALT  36859  bj-nsnid  37071  areacirclem4  37718  fdc  37752  dihglblem6  41342  itrere  42353  sn-inelr  42497  sn-itrere  42498  sn-retire  42499  pellexlem6  42845  pw2f1ocnv  43049  wepwsolem  43054  inaex  44316  axc5c4c711toc5  44421  lptioo2  45646  lptioo1  45647  1neven  48154