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  2108  axc10  2383  pwnss  5302  nsuceq0  6405  onssnel2i  6439  abnex  7713  ssonprc  7743  soseq  8115  dmtpos  8194  tfrlem15  8337  tz7.44-2  8352  tz7.48-3  8389  2pwuninel  9073  2pwne  9074  nnsdomg  9222  nnsdomgOLD  9223  r111  9704  r1pwss  9713  wfelirr  9754  rankxplim3  9810  carduni  9910  pr2neOLD  9934  alephle  10017  alephfp  10037  pwdjudom  10144  cfsuc  10186  fin23lem28  10269  fin23lem30  10271  isfin1-2  10314  ac5b  10407  zorn2lem4  10428  zorn2lem7  10431  cfpwsdom  10513  nd1  10516  nd2  10517  canthp1  10583  pwfseqlem1  10587  gchhar  10608  winalim2  10625  ltxrlt  11220  recgt0  12004  nnunb  12414  indstr  12851  wrdlen2i  14884  rlimno1  15596  lcmfnncl  16575  isprm2  16628  nprmdvds1  16652  divgcdodd  16656  coprm  16657  ramtcl2  16958  psgnunilem3  19410  torsubg  19768  prmcyg  19808  dprd2da  19958  prmirredlem  21414  pnfnei  23140  mnfnei  23141  1stccnp  23382  uzfbas  23818  ufinffr  23849  fin1aufil  23852  ovolunlem1a  25430  itg2gt0  25694  lgsquad2lem2  27329  dirith2  27472  noseponlem  27609  nosepssdm  27631  nodenselem8  27636  nolt02o  27640  nogt01o  27641  umgrnloop0  29089  usgrnloop0ALT  29185  nfrgr2v  30251  hon0  31772  ifeqeqx  32521  axsepg2ALT  35066  dfon2lem7  35770  bj-axc10v  36774  sbn1ALT  36839  bj-nsnid  37051  areacirclem4  37698  fdc  37732  dihglblem6  41327  sn-itrere  42469  sn-retire  42470  pellexlem6  42815  pw2f1ocnv  43019  wepwsolem  43024  inaex  44279  axc5c4c711toc5  44384  lptioo2  45622  lptioo1  45623  1neven  48219