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  2393  pwnss  5370  nsuceq0  6478  onssnel2i  6512  abnex  7792  ssonprc  7823  soseq  8200  dmtpos  8279  tfrlem15  8448  tz7.44-2  8463  tz7.48-3  8500  2pwuninel  9198  2pwne  9199  nnsdomg  9363  nnsdomgOLD  9364  r111  9844  r1pwss  9853  wfelirr  9894  rankxplim3  9950  carduni  10050  pr2neOLD  10074  alephle  10157  alephfp  10177  pwdjudom  10284  cfsuc  10326  fin23lem28  10409  fin23lem30  10411  isfin1-2  10454  ac5b  10547  zorn2lem4  10568  zorn2lem7  10571  cfpwsdom  10653  nd1  10656  nd2  10657  canthp1  10723  pwfseqlem1  10727  gchhar  10748  winalim2  10765  ltxrlt  11360  recgt0  12140  nnunb  12549  indstr  12981  wrdlen2i  14991  rlimno1  15702  lcmfnncl  16676  isprm2  16729  nprmdvds1  16753  divgcdodd  16757  coprm  16758  ramtcl2  17058  psgnunilem3  19538  torsubg  19896  prmcyg  19936  dprd2da  20086  prmirredlem  21506  pnfnei  23249  mnfnei  23250  1stccnp  23491  uzfbas  23927  ufinffr  23958  fin1aufil  23961  ovolunlem1a  25550  itg2gt0  25815  lgsquad2lem2  27447  dirith2  27590  noseponlem  27727  nosepssdm  27749  nodenselem8  27754  nolt02o  27758  nogt01o  27759  umgrnloop0  29144  usgrnloop0ALT  29240  nfrgr2v  30304  hon0  31825  ifeqeqx  32565  axsepg2ALT  35059  dfon2lem7  35753  bj-axc10v  36759  sbn1ALT  36824  bj-nsnid  37036  areacirclem4  37671  fdc  37705  dihglblem6  41297  itrere  42307  sn-inelr  42443  sn-itrere  42444  sn-retire  42445  pellexlem6  42790  pw2f1ocnv  42994  wepwsolem  42999  inaex  44266  axc5c4c711toc5  44371  lptioo2  45552  lptioo1  45553  1neven  47961